


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.