


default search action
20th FMCAD 2020: Haifa, Israel
- 2020 Formal Methods in Computer Aided Design, FMCAD 2020, Haifa, Israel, September 21-24, 2020. IEEE 2020, ISBN 978-3-85448-042-6

- Alexander Nadel

:
Anytime Algorithms for MaxSAT and Beyond. 1 - Peter Schrammel

:
The FMCAD 2020 Student Forum. 1 - Hillel Kugler:

Formal Verification for Natural and Engineered Biological Systems. 1 - Peter Schrammel:

How testable is business software? 1 - Orna Kupferman:

From Correctness to High Quality. 1 - Florian Lonsing, Subhasish Mitra

, Clark W. Barrett:
A Theoretical Framework for Symbolic Quick Error Detection. 1-10 - Armin Biere:

Tutorial on World-Level Model Checking. 1 - Alexander Fedotov, Jeroen J. A. Keiren, Julien Schmaltz:

Effective System Level Liveness Verification. 7-15 - Rohit Dureja, Jason Baumgartner, Robert Kanzelman, Mark Williams, Kristin Y. Rozier:

Accelerating Parallel Verification via Complementary Property Partitioning and Strategy Exploration. 16-25 - Tommy Tracy II, Lucas M. Tabajara, Moshe Y. Vardi, Kevin Skadron

:
Runtime Verification on FPGAs with LTLf Specifications. 36-46 - Prantik Chatterjee, Subhajit Roy, Bui Phi Diep, Akash Lal:

Distributed Bounded Model Checking. 47-56 - Denis Bueno, Arlen Cox, Karem A. Sakallah

:
EUFicient Reachability in Software with Arrays. 57-66 - Thomas Pani, Georg Weissenbacher

, Florian Zuleger:
Thread-modular Counter Abstraction for Parameterized Program Safety. 67-76 - Sepideh Asadi

, Martin Blicha
, Antti E. J. Hyvärinen, Grigory Fedyukovich, Natasha Sharygina
:
Incremental Verification by SMT-based Summary Repair. 77-82 - Alessandro Cimatti, Luca Geatti

, Nicola Gigante, Angelo Montanari, Stefano Tonetta:
Reactive Synthesis from Extended Bounded Response LTL Specifications. 83-92 - M. Fareed Arif, Daniel Larraz

, Mitziu Echeverria, Andrew Reynolds, Omar Chowdhury, Cesare Tinelli
:
SYSLITE: Syntax-Guided Synthesis of PLTL Formulas from Finite Traces. 93-103 - Rüdiger Ehlers, Ivan Gavran, Daniel Neider

:
Learning Properties in LTL ∩ ACTL from Positive Examples Only. 104-112 - Zichao Zhang, Arthur Azevedo de Amorim, Limin Jia

, Corina S. Pasareanu:
Automating Compositional Analysis of Authentication Protocols. 113-118 - Franz Brauße, Zurab Khasidashvili, Konstantin Korovin

:
Selecting Stable Safe Configurations for Systems Modelled by Neural Networks with ReLU Activation. 119-127 - Haoze Wu

, Alex Ozdemir, Aleksandar Zeljic, Kyle Julian, Ahmed Irfan, Divya Gopinath, Sadjad Fouladi, Guy Katz, Corina S. Pasareanu, Clark W. Barrett:
Parallelization Techniques for Verifying Neural Networks. 128-137 - Parand Alizadeh Alamdari, Guy Avni, Thomas A. Henzinger, Anna Lukina

:
Formal Methods with a Touch of Magic. 138-147 - Xuankang Lin, He Zhu, Roopsha Samanta, Suresh Jagannathan:

Art: Abstraction Refinement-Guided Training for Provably Correct Neural Networks. 148-157 - Lauren Pick, Grigory Fedyukovich, Aarti Gupta:

Automating Modular Verification of Secure Information Flow. 158-168 - Shuvendu K. Lahiri, Akash Lal, Sridhar Gopinath, Alexander Nutz, Vladimir Levin, Rahul Kumar, Nate Deisinger, Jakob Lichtenberg, Chetan Bansal:

Angelic Checking within Static Driver Verifier: Towards high-precision defects without (modeling) cost. 169-178 - Vasileios Klimis, George Parisis

, Bernhard Reus
:
Model Checking Software-Defined Networks with Flow Entries that Time Out. 179-184 - Byron Cook, Björn Döbel, Daniel Kroening, Norbert Manthey, Martin Pohlack, Elizabeth Polgreen, Michael Tautschnig, Pawel Wieczorkiewicz:

Using model checking tools to triage the severity of security bugs in the Xen hypervisor. 185-193 - Vincent Liew, Paul Beame

, Jo Devriendt, Jan Elffers, Jakob Nordström
:
Verifying Properties of Bit-vector Multiplication Using Cutting Planes Reasoning. 194-204 - Alexander Nadel

:
On Optimizing a Generic Function in SAT. 205-213 - Aina Niemetz

, Mathias Preiner:
Ternary Propagation-Based Local Search for more Bit-Precise Reasoning. 214-224 - Andrew Reynolds, Andres Nötzli, Clark W. Barrett, Cesare Tinelli

:
Reductions for Strings and Regular Expressions Revisited. 225-235 - Simon Jantsch, Hans Harder, Florian Funke

, Christel Baier
:
Switss: Computing Small Witnessing Subsystems. 236-244 - Yutaka Nagashima:

Smart Induction for Isabelle/HOL (Tool Paper). 245-254 - Pamina Georgiou, Bernhard Gleiss, Laura Kovács

:
Trace Logic for Inductive Loop Reasoning. 255-263 - Daniela Kaufmann

, Mathias Fleury, Armin Biere:
The Proof Checkers Pacheck and Pastèque for the Practical Algebraic Calculus. 264-269

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














