Hyperproperty Verification as CHC Satisfiability

Autor: Itzhaky, Shachar, Shoham, Sharon, Vizel, Yakir

Hyperproperties govern the behavior of a system or systems across multiple executions, and are being recognized as an important extension of regular temporal properties. So far, such properties have resisted comprehensive treatment by modern software

Externí odkaz: http://arxiv.org/abs/2304.12588

High-resolution CT phenotypes in pulmonary sarcoidosis: a multinational Delphi consensus study

Autor: Anderson, Adam, Morgenthau, Adam, Gaser, Adrian, Vizel, Alexander, Speranskaya, Alexandra, Gerke, Alicia, Goksel, Altinisik, Undurraga, Alvaro, Sharma, Amita, Oh, Andrea, Leung, Ann, Larici, Anna Rita, Prasse, Antje, Mazzei, Antonietta, Morais, Antonio, Bhalla, Ashu, Del Rio, Belen, Jankharia, Bhavin, Elicker, Brett, Pereira, Carlos, Biegelman-Aubry, Catherine, White, Charles, Ravaglia, Claudia, Hsia, Connie, Schaefer-Prokop, Cornelia, Launay, David, Talwar, Deepak, Castillo, Diego, Patel, Divya, Israel-Biet, Dominique, Valeyre, Dominique, Britt, Edward James, Bargagli, Elena, Bendstrup, Elisabeth, Crouser, Elliott, Nossent, Esther, Shmelev, Eugeny, Porquera, Eva Carmona, Bonella, Francesco, Cohen-Aubart, Fleur, Jeny, Florence, Ferrara, Giovanni, Jin, Gong Yong, Robbie, Hasti, Prosch, Helmut, Sumikawa, Hiromitsu, Ling-Pei, Ho, Lee, Ho Yun, Strambu, Irina, Buendia-Roldan, Ivette, Grutters, Jan, Ryu, Jay, Swigris, Jeff, Miedema, Jelle, Goo, Jin Mo, Barnett, Joseph, Verschakelen, Johny, Goldin, Jonathan, Seo, Joon Beom, Enghelmayer, Juan, Mana, Juan, Behr, Juergen, Patterson, Karen, Antoniou, Katerina, Brown, Kevin, Fujimoto, Kiminori, Savale, Laurent, Maier, Lisa, Richeldi, Luca, Neto, Manuel Lessa Ribeiro, Humbert, Marc, Judson, Marc, Veltkamp, Marcel, Wilsher, Margaret, Molina, Maria, Otaola, Maria, Revel, Marie-Pierre, Silva, Mario, Drent, Marjolein, Schiebler, Mark, Wijsenbeek-Lourens, Marlies, Bonifazi, Martina, Remy-Jardin, Martine, Koslow, Matthew, Balter, Meyer, Kreuter, Michael, Thillai, Muhunthan, Hamzeh, Nabeel, Chaudhuri, Nazia, Mogulkoc, Nesrin, Todd, Nevins, Screaton, Nick, Goh, Nicole, Shah, Nirav, Obi, Ogugua, Shlobin, Oksana, Baranova, Olga, Bresser, Paul, Rottoli, Paula, Brillet, Pierre-Yves, Said-Hartley, Qonita, Borie, Raphael, Mostard, Remy, van Zyl-smit, Richard, Kairalla, Ronaldo, Egashira, Ryoko, Boussouar, Samia, Lee, Sang Min, Bhalla, Sanjeev, Tomassetti, Sara, Quadrelli, Silvia, Hart, Simon P, Danoff, Sonye, Rajan, Sujeet, Choi, Sun Mi, Copley, Susan, Kim, Tae Jung, Johkoh, Takeshi, Corte, Tamera, McLoud, Theresa, Wessendorf, Thomas, Alfaro, Tiago, Arai, Toru, Costabel, Ulrich, Vicens-Zygmunt, Vanesa, Poletti, Venerino, Cottin, Vincent, Vucinic, Violeta, Wuyts, Wim, van Es, Wouter, Jeong, Yeon Joo, Inoue, Yoshikazu, Desai, Sujal R ^*, Sivarasan, Nishanth, Johannson, Kerri A, George, Peter M, Culver, Daniel A, Devaraj, Anand, Lynch, David A, Milne, David, Renzoni, Elisabetta, Nunes, Hilario, Sverzellati, Nicola, Spagnolo, Paolo, Baughman, Robert P, Yadav, Ruchi, Piciucchi, Sara, Walsh, Simon L F, Kouranos, Vasileios, Wells, Athol U

Publikováno v: In The Lancet Respiratory Medicine May 2024 12(5):409-418

Quantifiers on Demand

Autor: Gurfinkel, Arie, Shoham, Sharon, Vizel, Yakir

Automated program verification is a difficult problem. It is undecidable even for transition systems over Linear Integer Arithmetic (LIA). Extending the transition system with theory of Arrays, further complicates the problem by requiring inference a

Externí odkaz: http://arxiv.org/abs/2106.00664

Analysis of Management of Patients with COVID-19 in a Temporary Infectious Diseases Hospital Deployed on the Facilities of Republican TB Dispensary, the Republic of Tatarstan

Autor: A. A. Vizel, S. A. Shayakhmetova, A. P. Alekseev, I. Yu. Vizel, A. V. Nikitin, A. A. Galimov

Publikováno v: Туберкулез и болезни лёгких, Vol 100, Iss 8, Pp 6-17 (2022)

COVID-19 is a viral infection and its prevalence requires investigation of different co-morbid conditions including tuberculosis, as well as operation of temporary infectious diseases hospitals (TIDH) for the treatment of COVID-19 deployed on the fac

Externí odkaz: https://doaj.org/article/1780d9fa94214331a819ec999feedcf6

Property Directed Self Composition

Autor: Shemer, Ron, Gurfinkel, Arie, Shoham, Sharon, Vizel, Yakir

We address the problem of verifying k-safety properties: properties that refer to k-interacting executions of a program. A prominent way to verify k-safety properties is by self composition. In this approach, the problem of checking k-safety over the

Externí odkaz: http://arxiv.org/abs/1905.07705