


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.


Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID














