Abstract is missing.
- The FMCAD 2020 Student ForumPeter Schrammel. 1 [doi]
- Formal Verification for Natural and Engineered Biological SystemsHillel Kugler. 1 [doi]
- A Theoretical Framework for Symbolic Quick Error DetectionFlorian Lonsing, Subhasish Mitra, Clark W. Barrett. 1-10 [doi]
- How testable is business software?Peter Schrammel. 1 [doi]
- Anytime Algorithms for MaxSAT and BeyondAlexander Nadel. 1 [doi]
- Tutorial on World-Level Model CheckingArmin Biere. 1 [doi]
- From Correctness to High QualityOrna Kupferman. 1 [doi]
- Effective System Level Liveness VerificationAlexander Fedotov, Jeroen J. A. Keiren, Julien Schmaltz. 7-15 [doi]
- Accelerating Parallel Verification via Complementary Property Partitioning and Strategy ExplorationRohit Dureja, Jason Baumgartner, Robert Kanzelman, Mark Williams, Kristin Y. Rozier. 16-25 [doi]
- Runtime Verification on FPGAs with LTLf SpecificationsTommy Tracy II, Lucas M. Tabajara, Moshe Y. Vardi, Kevin Skadron. 36-46 [doi]
- Distributed Bounded Model CheckingPrantik Chatterjee, Subhajit Roy, Bui Phi Diep, Akash Lal. 47-56 [doi]
- EUFicient Reachability in Software with ArraysDenis Bueno, Arlen Cox, Karem A. Sakallah. 57-66 [doi]
- Thread-modular Counter Abstraction for Parameterized Program SafetyThomas Pani, Georg Weissenbacher, Florian Zuleger. 67-76 [doi]
- Incremental Verification by SMT-based Summary RepairSepideh Asadi, Martin Blicha, Antti E. J. Hyvärinen, Grigory Fedyukovich, Natasha Sharygina. 77-82 [doi]
- Reactive Synthesis from Extended Bounded Response LTL SpecificationsAlessandro Cimatti, Luca Geatti, Nicola Gigante, Angelo Montanari, Stefano Tonetta. 83-92 [doi]
- SYSLITE: Syntax-Guided Synthesis of PLTL Formulas from Finite TracesM. Fareed Arif, Daniel Larraz, Mitziu Echeverria, Andrew Reynolds, Omar Chowdhury, Cesare Tinelli. 93-103 [doi]
- Learning Properties in LTL ∩ ACTL from Positive Examples OnlyRüdiger Ehlers, Ivan Gavran, Daniel Neider. 104-112 [doi]
- Automating Compositional Analysis of Authentication ProtocolsZichao Zhang, Arthur Azevedo de Amorim, Limin Jia 0001, Corina S. Pasareanu. 113-118 [doi]
- Selecting Stable Safe Configurations for Systems Modelled by Neural Networks with ReLU ActivationFranz Brauße, Zurab Khasidashvili, Konstantin Korovin. 119-127 [doi]
- Parallelization Techniques for Verifying Neural NetworksHaoze Wu 0001, Alex Ozdemir, Aleksandar Zeljic, Kyle Julian, Ahmed Irfan, Divya Gopinath, Sadjad Fouladi, Guy Katz, Corina S. Pasareanu, Clark W. Barrett. 128-137 [doi]
- Formal Methods with a Touch of MagicParand Alizadeh Alamdari, Guy Avni, Thomas A. Henzinger, Anna Lukina. 138-147 [doi]
- Art: Abstraction Refinement-Guided Training for Provably Correct Neural NetworksXuankang Lin, He Zhu 0001, Roopsha Samanta, Suresh Jagannathan. 148-157 [doi]
- Automating Modular Verification of Secure Information FlowLauren Pick, Grigory Fedyukovich, Aarti Gupta. 158-168 [doi]
- Angelic Checking within Static Driver Verifier: Towards high-precision defects without (modeling) costShuvendu K. Lahiri, Akash Lal, Sridhar Gopinath, Alexander Nutz, Vladimir Levin, Rahul Kumar 0002, Nate Deisinger, Jakob Lichtenberg, Chetan Bansal. 169-178 [doi]
- Model Checking Software-Defined Networks with Flow Entries that Time OutVasileios Klimis, George Parisis, Bernhard Reus. 179-184 [doi]
- Using model checking tools to triage the severity of security bugs in the Xen hypervisorByron Cook, Björn Döbel, Daniel Kroening, Norbert Manthey, Martin Pohlack, Elizabeth Polgreen, Michael Tautschnig, Pawel Wieczorkiewicz. 185-193 [doi]
- Verifying Properties of Bit-vector Multiplication Using Cutting Planes ReasoningVincent Liew, Paul Beame, Jo Devriendt, Jan Elffers, Jakob Nordström. 194-204 [doi]
- On Optimizing a Generic Function in SATAlexander Nadel. 205-213 [doi]
- Ternary Propagation-Based Local Search for more Bit-Precise ReasoningAina Niemetz, Mathias Preiner. 214-224 [doi]
- Reductions for Strings and Regular Expressions RevisitedAndrew Reynolds, Andres Nötzli, Clark W. Barrett, Cesare Tinelli. 225-235 [doi]
- Switss: Computing Small Witnessing SubsystemsSimon Jantsch, Hans Harder, Florian Funke 0002, Christel Baier. 236-244 [doi]
- Smart Induction for Isabelle/HOL (Tool Paper)Yutaka Nagashima. 245-254 [doi]
- Trace Logic for Inductive Loop ReasoningPamina Georgiou, Bernhard Gleiss, Laura Kovács. 255-263 [doi]
- The Proof Checkers Pacheck and Pastèque for the Practical Algebraic CalculusDaniela Kaufmann, Mathias Fleury, Armin Biere. 264-269 [doi]