Abstract is missing.
- Why Do Things Go Wrong (or Right)? Applications of Causal Reasoning to VerificationHana Chockler. 1 [doi]
- Automating Geometric Proofs of Collision Avoidance with Active CornersNishant Kheterpal, Elanor Tang, Jean-Baptiste Jeannin. 1-10 [doi]
- Reconciling Verified-Circuit Development and Verilog DevelopmentAndreas Lööw. 1-10 [doi]
- Learning Deterministic Finite Automata Decompositions from Examples and DemonstrationsNiklas Lauffer, Beyazit Yalcinkaya, Marcell Vazquez-Chanlatte, Ameesh Shah, Sanjit A. Seshia. 1-6 [doi]
- Divider Verification Using Symbolic Computer Algebra and Delayed Don't Care OptimizationAlexander Konrad, Christoph Scholl 0001, Alireza Mahzoon, Daniel Große, Rolf Drechsler. 1-10 [doi]
- On Applying Model Checking in Formal VerificationHåkan Hjort. 1 [doi]
- The seL4 Verification Journey: How Have the Challenges and Opportunities EvolvedJune Andronick. 1 [doi]
- Verification of Distributed Protocols: Decidable Modeling and Invariant InferenceOded Padon. 4 [doi]
- 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]
- Verification-Aided Deep Ensemble SelectionGuy Amir, Tom Zelazny, Guy Katz, Michael Schapira. 27-37 [doi]
- Neural Network Verification with Proof ProductionOmri Isac, Clark W. Barrett, Min Zhang 0002, Guy Katz. 38-48 [doi]
- Tbuddy: A Proof-Generating BDD PackageRandal E. Bryant. 49-58 [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]
- Timed Causal Fanin Analysis for Symbolic Circuit SimulationRoope Kaivola, Neta Bar Kama. 99-107 [doi]
- Formally Verified Isolation of DMAJonas Haglund, Roberto Guanciale. 118-128 [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]
- Error Correction Code Algorithm and Implementation Verification Using Symbolic RepresentationsAarti Gupta, Roope Kaivola, Mihir Parang Mehta, Vaibhav Singh. 151-159 [doi]
- First-Order Subsumption via SAT SolvingJakob Rath, Armin Biere, Laura Kovács. 160-169 [doi]
- BaxMC: a CEGAR approach to Max#SATThomas Vigouroux, Cristian Ene, David Monniaux, Laurent Mounier, Marie-Laure Potet. 170-178 [doi]
- Compact Symmetry Breaking for TournamentsEvan Lohn, Chris Lambert, Marijn J. H. Heule. 179-188 [doi]
- Enumerative Data Types with ConstraintsAndrew T. Walter, David A. Greve, Panagiotis Manolios. 189-198 [doi]
- Reducing NEXP-complete problems to DQBFFa-Hsun Chen, Shen-Chang Huang, Yu-Cheng Lu, Tony Tan. 199-204 [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]
- Automatic Repair and Deadlock Detection for Parameterized SystemsSwen Jacobs, Mouhammad Sakr, Marcus Völp. 225-234 [doi]
- Synthesizing Locally Symmetric Parameterized Protocols from Temporal SpecificationsRuoxi Zhang, Richard J. Trefler, Kedar S. Namjoshi. 235-244 [doi]
- Synthesizing Self-Stabilizing Parameterized Protocols with Unbounded VariablesAli Ebnenasir. 245-254 [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]
- +William Schultz, Ian Dardik, Stavros Tripakis. 273-283 [doi]
- Awaiting for Godot: Stateless Model Checking that Avoids Executions where Nothing HappensBengt Jonsson 0001, Magnus Lång, Konstantinos Sagonas. 284-293 [doi]
- Synthesizing Transducers from Complex SpecificationsAnvay Grover, Ruediger Ehlers, Loris D'Antoni. 294-303 [doi]
- Synthesis of Semantic Actions in Attribute GrammarsPankaj Kumar Kalita, Miriyala Jeevan Kumar, Subhajit Roy 0001. 304-314 [doi]
- Reactive Synthesis Modulo Theories using Abstraction RefinementBenedikt Maderbacher, Roderick Bloem. 315-324 [doi]
- Automated Conversion of Axiomatic to Operational Models: Theory and PracticeAdwait Godbole, Yatin A. Manerkar, Sanjit A. Seshia. 331-342 [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]
- Tricera: Verifying C Programs Using the Theory of HeapsZafer Esen, Philipp Rümmer. 380-391 [doi]