| Bassan, Shahaf; Amir, Guy; Corsi, Davide; Refaeli, Idan; Katz, Guy |
Formally Explaining Neural Networks within Reactive Systems |
|
| Li, Bohan; Cai, Shaowei |
Local Search For SMT On Linear and Multilinear Real Arithmetic |
|
| Lam, Kait; Coughlin, Nicholas |
Lift-off: Trustworthy ARMv8 semantics from formal specifications |
|
| Yu, Emily; Froleyks, Nils; Biere, Armin; Heljanko, Keijo |
Towards Compositional Hardware Model Checking Certification |
|
| Zhou, Yi; Bosamiya, Jay; Takashima, Yoshiki; Li, Jessica G; Heule, Marijn J.H.; Parno, Bryan |
Mariposa: Measuring SMT Instability in Automated Program Verification |
|
| Larraz, Daniel; Lorch, Robert M; Yahyazadeh, Moosa; Arif, M. Fareed; Chowdhury, Omar; Tinelli, Cesare |
CRV: An Automated Resiliency Reasoner for System Design Models |
|
| Mohamed, Abdalrhman M; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare |
A Procedure for SyGuS Solution Fitting via Matching and Rewrite Rule Discovery |
|
| Meng, Baoluo; Debnath, Joyanta; Varanasi, Sarat Chandra; Manolios, Emmanuel; Durling, Michael; Paul, Saswata; Prince, Daniel; Alsabbagh, Saif; Haadsma, Richard; McMillan, Craig; Zhang, Chi; Oates, Tim |
Towards a Correct-by-Construction Design of Integrated Modular Avionics |
|
| Wilson, Amalee D; Noetzli, Andres P; Reynolds, Andrew; Cook, Byron; Tinelli, Cesare; Barrett, Clark |
Partitioning Strategies for Distributed SMT Solving |
|
| Wu, Haoze; Hahn, Christopher; Lonsing, Florian; Mann, Makai; Ramanujan, Raghuram; Barrett, Clark |
Lightweight Online Learning for Sets of Related Problems in Automated Reasoning |
|
| Coward, Samuel; Morini, Emiliano; Tan, Bryan; Drane, Theo; Constantinides, George |
Datapath Verification via Word-Level E-Graph Rewriting |
|
| Dong, Ning; Guanciale, Roberto; Dam, Mads; Lööw, Andreas |
Formal Verification of Correctness and Information Flow Security for an In-Order Pipelined Processor |
|
| Park, Kanghee; Johnson, Keith J C; D’Antoni, Loris; Reps, Thomas |
Modular System Synthesis |
|
| Elsaleh, Raya; Katz, Guy |
Delta-Debugging Neural Network Verifiers |
|
| Zhang, Changjian; Dardik, Ian; Meira-Góes, Rômulo; Garlan, David; Kang, Eunsuk |
Fortis: A Tool for Analysis and Repair of Robust Software Systems |
|
| Froleyks, Nils; Yu, Emily; Biere, Armin |
BIG Backbones |
|
| Kiesl-Reiter, Benjamin; Whalen, Michael W |
Proofs for Incremental SAT with Inprocessing |
|
| Codel, Cayden R; Avigad, Jeremy; Heule, Marijn J.H. |
Verified Encodings for SAT Solvers |
|
| Tollec, Simon; Asavoae, Mihail; Couroussé, Damien; Heydemann, Karine; Jan, Mathieu |
µArchiFI: Formal Modeling and Verification Strategies for Microarchitetural Fault Injections |
|
| Marmanis, Iason; Vafeiadis, Viktor |
Optimal Bounded Partial Order Reduction |
|
| Tafese, Joseph; Gurfinkel, Arie; Garcia-Contreras, Isabel |
Btor2MLIR: A Format for Hardware Verification |
|
| Taylor, Landon J; Israelsen, Bryant; Zhang, Zhen |
Cycle and Commute: Rare-Event Probability Verification for Chemical Reaction Networks |
|
| Bernardes Fernandes Ferreira, Nikson; Moscato, Mariano M; Titolo, Laura; Ayala-Rincon, Mauricio |
A provably correct floating-point implementation of Well Clear Avionics Concepts |
|
| Sakallah, Karem A; Fazekas, Katalin; Goel, Aman |
SAT-Based Quantified Symmetric Minimization of the Reachable States of Distributed Protocols |
|
| Ryan, Kaki; Sturton, Cynthia |
Countering the Path Explosion Problem in the Symbolic Execution of Hardware Designs |
|
| Qin, Xin; Hashemi, Navid; Lindemann, Lars; Deshmukh, Jyotirmoy |
Conformance Testing for Stochastic Cyber-Physical Systems |
|
| Godbole, Adwait; Ye, Leiqi; Manerkar, Yatin A.; Seshia, Sanjit A. |
Modelling and Verification of Security-Oriented Resource Partitioning Schemes |
|
| Saxena, Manasvi; Song, Shuang; Sha, Lui |
MediK: Towards Safe Guideline-based Clinical Decision Support |
|
| Thakkar, Arkesh H; D’Souza, Deepak |
Data-Driven Learning of Strong Conjunctive Invariants |
|
| Bhat, Shreesha G.; Nagar, Kartik |
Automating Cutoff-based Verification of Distributed Protocols |
|
| Pastva, Samuel; Henzinger, Thomas |
Binary decision diagrams on modern hardware |
|
