default search action
22nd FMCAD 2022: Trento, Italy
- Alberto Griggio, Neha Rungta:
22nd Formal Methods in Computer-Aided Design, FMCAD 2022, Trento, Italy, October 17-21, 2022. IEEE 2022, ISBN 978-3-85448-053-2 - Hana Chockler:
Why Do Things Go Wrong (or Right)? Applications of Causal Reasoning to Verification. 1 - Håkan Hjort:
On Applying Model Checking in Formal Verification. 1 - Nishant Kheterpal, Elanor Tang, Jean-Baptiste Jeannin:
Automating Geometric Proofs of Collision Avoidance with Active Corners. 1-10 - Alexander Konrad, Christoph Scholl, Alireza Mahzoon, Daniel Große, Rolf Drechsler:
Divider Verification Using Symbolic Computer Algebra and Delayed Don't Care Optimization. 1-10 - Andreas Lööw:
Reconciling Verified-Circuit Development and Verilog Development. 1-10 - Niklas Lauffer, Beyazit Yalcinkaya, Marcell Vazquez-Chanlatte, Ameesh Shah, Sanjit A. Seshia:
Learning Deterministic Finite Automata Decompositions from Examples and Demonstrations. 1-6 - June Andronick:
The seL4 Verification Journey: How Have the Challenges and Opportunities Evolved. 1 - Oded Padon:
Verification of Distributed Protocols: Decidable Modeling and Invariant Inference. 4 - Mathias Preiner:
The FMCAD 2022 Student Forum. 5-6 - Yannan Li, Jingbo Wang, Chao Wang:
Proving Robustness of KNN Against Adversarial Data Poisoning. 7-16 - Tom Zelazny, Haoze Wu, Clark W. Barrett, Guy Katz:
On Optimizing Back-Substitution Methods for Neural Network Verification. 17-26 - Guy Amir, Tom Zelazny, Guy Katz, Michael Schapira:
Verification-Aided Deep Ensemble Selection. 27-37 - Omri Isac, Clark W. Barrett, Min Zhang, Guy Katz:
Neural Network Verification with Proof Production. 38-48 - Randal E. Bryant:
Tbuddy: A Proof-Generating BDD Package. 49-58 - Emily Yu, Nils Froleyks, Armin Biere, Keijo Heljanko:
Stratified Certification for k-Induction. 59-64 - Andres Nötzli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language. 65-74 - Oliver Flatt, Samuel Coward, Max Willsey, Zachary Tatlock, Pavel Panchekha:
Small Proofs from Congruence Closure. 75-83 - Abhishek Anil Nair, Saranyu Chattopadhyay, Haoze Wu, Alex Ozdemir, Clark W. Barrett:
Proof-Stitch: Proof Combination for Divide-and-Conquer SAT Solvers. 84-88 - Roope Kaivola, Neta Bar Kama:
Timed Causal Fanin Analysis for Symbolic Circuit Simulation. 99-107 - Jonas Haglund, Roberto Guanciale:
Formally Verified Isolation of DMA. 118-128 - Karl Palmskog, Xiaomo Yao, Ning Dong, Roberto Guanciale, Mads Dam:
Foundations and Tools in HOL4 for Analysis of Microarchitectural Out-of-Order Execution. 129-138 - Ross Daly, Caleb Donovick, Jackson Melchert, Rajsekhar Setaluri, Nestan Tsiskaridze, Priyanka Raina, Clark W. Barrett, Pat Hanrahan:
Synthesizing Instruction Selection Rewrite Rules from RTL using SMT. 139-150 - Aarti Gupta, Roope Kaivola, Mihir Parang Mehta, Vaibhav Singh:
Error Correction Code Algorithm and Implementation Verification Using Symbolic Representations. 151-159 - Jakob Rath, Armin Biere, Laura Kovács:
First-Order Subsumption via SAT Solving. 160-169 - Thomas Vigouroux, Cristian Ene, David Monniaux, Laurent Mounier, Marie-Laure Potet:
BaxMC: a CEGAR approach to Max#SAT. 170-178 - Evan Lohn, Chris Lambert, Marijn J. H. Heule:
Compact Symmetry Breaking for Tournaments. 179-188 - Andrew T. Walter, David A. Greve, Panagiotis Manolios:
Enumerative Data Types with Constraints. 189-198 - Fa-Hsun Chen, Shen-Chang Huang, Yu-Cheng Lu, Tony Tan:
Reducing NEXP-complete problems to DQBF. 199-204 - Suwei Yang, Victor C. Liang, Kuldeep S. Meel:
INC: A Scalable Incremental Weighted Sampler. 205-213 - Siddharth Priya, Yusen Su, Yuyan Bao, Xiang Zhou, Yakir Vizel, Arie Gurfinkel:
Bounded Model Checking for LLVM. 214-224 - Swen Jacobs, Mouhammad Sakr, Marcus Völp:
Automatic Repair and Deadlock Detection for Parameterized Systems. 225-234 - Ruoxi Zhang, Richard J. Trefler, Kedar S. Namjoshi:
Synthesizing Locally Symmetric Parameterized Protocols from Temporal Specifications. 235-244 - Ali Ebnenasir:
Synthesizing Self-Stabilizing Parameterized Protocols with Unbounded Variables. 245-254 - Pamina Georgiou, Bernhard Gleiss, Ahmed Bhayat, Michael Rawson, Laura Kovács, Giles Reger:
The Rapid Software Verification Framework. 255-260 - Divya Raghunathan, Ryan Beckett, Aarti Gupta, David Walker:
ACORN: Network Control Plane Abstraction using Route Nondeterminism. 261-272 - William Schultz, Ian Dardik, Stavros Tripakis:
Plain and Simple Inductive Invariant Inference for Distributed Protocols in TLA+. 273-283 - Bengt Jonsson, Magnus Lång, Konstantinos Sagonas:
Awaiting for Godot: Stateless Model Checking that Avoids Executions where Nothing Happens. 284-293 - Anvay Grover, Ruediger Ehlers, Loris D'Antoni:
Synthesizing Transducers from Complex Specifications. 294-303 - Pankaj Kumar Kalita, Miriyala Jeevan Kumar, Subhajit Roy:
Synthesis of Semantic Actions in Attribute Grammars. 304-314 - Benedikt Maderbacher, Roderick Bloem:
Reactive Synthesis Modulo Theories using Abstraction Refinement. 315-324 - Adwait Godbole, Yatin A. Manerkar, Sanjit A. Seshia:
Automated Conversion of Axiomatic to Operational Models: Theory and Practice. 331-342 - Mario Bucev, Viktor Kuncak:
Formally Verified Quite OK Image Format. 343-348 - Martin Blicha, Grigory Fedyukovich, Antti E. J. Hyvärinen, Natasha Sharygina:
Split Transition Power Abstraction for Unbounded Safety. 349-358 - Anders Schlichtkrull, Morten Konggaard Schou, Jirí Srba, Dmitriy Traytel:
Differential Testing of Pushdown Reachability with a Formally Verified Oracle. 369-379 - Zafer Esen, Philipp Rümmer:
Tricera: Verifying C Programs Using the Theory of Heaps. 380-391
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.