Zobrazeno 1 - 10
of 633
pro vyhledávání: '"A A, Vizel'"'
We present CureSpec, the first model-checking based framework for automatic repair of programs with respect to information leaks in the presence of side-channels and speculative execution. CureSpec is based on formal models of attacker capabilities,
Externí odkaz:
http://arxiv.org/abs/2305.10092
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
A recent case study from AWS by Chong et al. proposes an effective methodology for Bounded Model Checking in industry. In this paper, we report on a follow up case study that explores the methodology from the perspective of three research questions:
Externí odkaz:
http://arxiv.org/abs/2107.00723
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
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
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
The principle of strong induction, also known as k-induction is one of the first techniques for unbounded SAT-based Model Checking (SMC). While elegant and simple to apply, properties as such are rarely k-inductive and when they can be strengthened,
Externí odkaz:
http://arxiv.org/abs/1906.01583
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
Publikováno v:
Туберкулез и болезни лёгких, Vol 100, Iss 1, Pp 7-18 (2022)
The article analyzes 46 publications on the use of ICS for COVID-19. Both research results and their discussion by specialists are presented. The expediency of continuing basic therapy, including ICS, has been demonstrated in the event of COVID-19 in
Externí odkaz:
https://doaj.org/article/71aab7a5ee914098af9a5c60afcabce9
Autor:
Huang, Bo-Yuan, Zhang, Hongce, Subramanyan, Pramod, Vizel, Yakir, Gupta, Aarti, Malik, Sharad
Modern Systems-on-Chip (SoC) designs are increasingly heterogeneous and contain specialized semi-programmable accelerators in addition to programmable processors. In contrast to the pre-accelerator era, when the ISA played an important role in verifi
Externí odkaz:
http://arxiv.org/abs/1801.01114