Abstract is missing.
- The FMCAD 2022 Student ForumMathias Preiner. 5-6 [doi]
- Proving Robustness of KNN Against Adversarial Data PoisoningYannan Li, Jingbo Wang 0006, Chao Wang 0001. 7-16 [doi]
- On Optimizing Back-Substitution Methods for Neural Network VerificationTom Zelazny, Haoze Wu 0001, Clark W. Barrett, Guy Katz. 17-26 [doi]
- Neural Network Verification with Proof ProductionOmri Isac, Clark W. Barrett, Min Zhang 0002, Guy Katz. 38-48 [doi]
- Stratified Certification for k-InductionEmily Yu, Nils Froleyks, Armin Biere, Keijo Heljanko. 59-64 [doi]
- Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific LanguageAndres Nötzli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds 0001, Clark W. Barrett, Cesare Tinelli. 65-74 [doi]
- Small Proofs from Congruence ClosureOliver Flatt, Samuel Coward, Max Willsey, Zachary Tatlock, Pavel Panchekha. 75-83 [doi]
- Proof-Stitch: Proof Combination for Divide-and-Conquer SAT SolversAbhishek Anil Nair, Saranyu Chattopadhyay, Haoze Wu 0001, Alex Ozdemir, Clark W. Barrett. 84-88 [doi]
- Foundations and Tools in HOL4 for Analysis of Microarchitectural Out-of-Order ExecutionKarl Palmskog, Xiaomo Yao, Ning Dong, Roberto Guanciale, Mads Dam. 129-138 [doi]
- Synthesizing Instruction Selection Rewrite Rules from RTL using SMTRoss Daly, Caleb Donovick, Jackson Melchert, Rajsekhar Setaluri, Nestan Tsiskaridze, Priyanka Raina, Clark W. Barrett, Pat Hanrahan. 139-150 [doi]
- Enumerative Data Types with ConstraintsAndrew T. Walter, David A. Greve, Panagiotis Manolios. 189-198 [doi]
- INC: A Scalable Incremental Weighted SamplerSuwei Yang, Victor C. Liang, Kuldeep S. Meel. 205-213 [doi]
- Bounded Model Checking for LLVMSiddharth Priya, Yusen Su, Yuyan Bao, Xiang Zhou, Yakir Vizel, Arie Gurfinkel. 214-224 [doi]
- The Rapid Software Verification FrameworkPamina Georgiou, Bernhard Gleiss, Ahmed Bhayat, Michael Rawson 0001, Laura Kovács, Giles Reger. 255-260 [doi]
- ACORN: Network Control Plane Abstraction using Route NondeterminismDivya Raghunathan, Ryan Beckett, Aarti Gupta, David Walker 0001. 261-272 [doi]
- Awaiting for Godot: Stateless Model Checking that Avoids Executions where Nothing HappensBengt Jonsson 0001, Magnus Lång, Konstantinos Sagonas. 284-293 [doi]
- Synthesis of Semantic Actions in Attribute GrammarsPankaj Kumar Kalita, Miriyala Jeevan Kumar, Subhajit Roy 0001. 304-314 [doi]
- Formally Verified Quite OK Image FormatMario Bucev, Viktor Kuncak. 343-348 [doi]
- Split Transition Power Abstraction for Unbounded SafetyMartin Blicha, Grigory Fedyukovich, Antti E. J. Hyvärinen, Natasha Sharygina. 349-358 [doi]
- Differential Testing of Pushdown Reachability with a Formally Verified OracleAnders Schlichtkrull, Morten Konggaard Schou, Jirí Srba, Dmitriy Traytel. 369-379 [doi]