Abstract is missing.
- A Billion SMT Queries a Day (Invited Paper)Neha Rungta. 3-18 [doi]
- Program Verification with Constrained Horn Clauses (Invited Paper)Arie Gurfinkel. 19-29 [doi]
- Data-Driven Invariant Learning for Probabilistic ProgramsJialu Bao, Nitesh Trivedi, Drashti Pathak, Justin Hsu, Subhajit Roy. 33-54 [doi]
- Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic ProgramsKrishnendu Chatterjee, Amir Kafshdar Goharshady, Tobias Meggendorfer, Dorde Zikelic. 55-78 [doi]
- Does a Program Yield the Right Distribution? - Verifying Probabilistic Programs via Generating FunctionsMingshuai Chen, Joost-Pieter Katoen, Lutz Klinkenberg, Tobias Winkler. 79-101 [doi]
- Abstraction-Refinement for Hierarchical Probabilistic ModelsSebastian Junges, Matthijs T. J. Spaan. 102-123 [doi]
- Shared Certificates for Neural Network VerificationMarc Fischer 0002, Christian Sprecher, Dimitar I. Dimitrov, Gagandeep Singh 0001, Martin T. Vechev. 127-148 [doi]
- Example Guided Synthesis of Linear Approximations for Neural Network VerificationBrandon Paulsen, Chao Wang 0001. 149-170 [doi]
- Verifying Neural Networks Against Backdoor AttacksLong H. Pham, Jun Sun 0001. 171-192 [doi]
- Trainify: A CEGAR-Driven Training and Verification Framework for Safe Deep Reinforcement LearningPeng Jin, Jiaxu Tian, Dapeng Zhi, Xuejun Wen, Min Zhang. 193-218 [doi]
- Neural Network Robustness as a Verification Property: A Principled Case StudyMarco Casadio, Ekaterina Komendantskaya, Matthew L. Daggitt, Wen Kokke, Guy Katz, Guy Amir, Idan Refaeli. 219-231 [doi]
- The Lattice-Theoretic Essence of Property Directed Reachability AnalysisMayuko Kori, Natsuki Urabe, Shin-ya Katsumata, Kohei Suenaga, Ichiro Hasuo. 235-256 [doi]
- Affine Loop Invariant Generation via Matrix AlgebraYucheng Ji, Hongfei Fu 0001, Bin Fang, Haibo Chen 0001. 257-281 [doi]
- Data-driven Numerical Invariant Synthesis with Automatic Generation of AttributesAhmed Bouajjani, Wael-Amine Boutglay, Peter Habermehl. 282-303 [doi]
- Proof-Guided Underapproximation Widening for Bounded Model CheckingPrantik Chatterjee, Jaydeepsinh Meda, Akash Lal, Subhajit Roy. 304-324 [doi]
- SolCMC: Solidity Compiler's Model CheckerLeonardo Alt, Martin Blicha, Antti E. J. Hyvärinen, Natasha Sharygina. 325-338 [doi]
- Software Verification of Hyperproperties Beyond k-SafetyRaven Beutner, Bernd Finkbeiner. 341-362 [doi]
- A Scalable Shannon Entropy EstimatorPriyanka Golia, Brendan Juba, Kuldeep S. Meel. 363-384 [doi]
- PoS4MPC: Automated Security Policy Synthesis for Secure Multi-party ComputationYuxin Fan, Fu Song, Taolue Chen, Liangfeng Zhang, Wanwei Liu. 385-406 [doi]
- Explaining Hyperproperty ViolationsNorine Coenen, Raimund Dachselt, Bernd Finkbeiner, Hadar Frenkel, Christopher Hahn, Tom Horak, Niklas Metzger, Julian Siber. 407-429 [doi]
- Distilling Constraints in Zero-Knowledge ProtocolsElvira Albert, Marta Bellés-Muñoz, Miguel Isabel, Clara Rodríguez-Núñez, Albert Rubio. 430-443 [doi]
- Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic EncryptionRyotaro Banno, Kotaro Matsuoka, Naoki Matsumoto, Song Bian 0001, Masaki Waga, Kohei Suenaga. 447-468 [doi]
- Abstraction Modulo Stability for Reverse EngineeringAnna Becchi, Alessandro Cimatti. 469-489 [doi]
- Reachability of Koopman Linearized Systems Using Random Fourier Feature Observables and Polynomial Zonotope RefinementStanley Bak, Sergiy Bogomolov, Brandon Hencey, Niklas Kochdumper, Ethan Lew, Kostiantyn Potomkin. 490-510 [doi]
- RINO: Robust INner and Outer Approximated Reachability of Neural Networks Controlled SystemsEric Goubault, Sylvie Putot. 511-523 [doi]
- STLmc: Robust STL Model Checking of Hybrid Systems Using SMTGeunyeol Yu, Jia Lee, Kyungmin Bae. 524-537 [doi]
- UCLID5: Multi-modal Formal Modeling, Verification, and SynthesisElizabeth Polgreen, Kevin Cheang, Pranav Gaddamadugu, Adwait Godbole, Kevin Laeufer, Shaokai Lin, Yatin A. Manerkar, Federico Mora, Sanjit A. Seshia. 538-551 [doi]