Philipp Rümmer

Marc Brockschmidt

CoRR, 2022

An SMT-LIB Theory of Heaps.

[BibT_eX]

[DOI]

Proceedings of the 20th Internal Workshop on Satisfiability Modulo Theories co-located with the 11th International Joint Conference on Automated Reasoning (IJCAR 2022) part of the 8th Federated Logic Conference (FLoC 2022), 2022

Exploring Representation of Horn clauses using GNNs.

[BibT_eX]

[DOI]

Chencheng Liang

Marc Brockschmidt

Proceedings of the Workshop on Practical Aspects of Automated Reasoning Co-located with the 11th International Joint Conference on Automated Reasoning (FLoC/IJCAR 2022), Haifa, Israel, August, 11, 2022

TriCo - Triple Co-piloting of Implementation, Specification and Tests.

[BibT_eX]

[DOI]

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles, 2022

Poster Abstract: Scheduling Dynamic Software Updates in Safety-critical Embedded Systems - the Case of Aerial Drones.

[BibT_eX]

[DOI]

Proceedings of the 13th ACM/IEEE International Conference on Cyber-Physical Systems, 2022

Tricera: Verifying C Programs Using the Theory of Heaps.

[BibT_eX]

[DOI]

Proceedings of the 22nd Formal Methods in Computer-Aided Design, 2022

NeRTA: Enabling Dynamic Software Updates in Mobile Robotics.

[BibT_eX]

[DOI]

Proceedings of the 2022 International Conference on Embedded Wireless Systems and Networks, 2022

CertiStr: a certified string solver.

[BibT_eX]

[DOI]

Proceedings of the CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17, 2022

Alice in Wineland: A Fairy Tale with Contracts.

[BibT_eX]

[DOI]

Dilian Gurov

Christian Lidström

Proceedings of the Logic of Software. A Tasting Menu of Formal Methods, 2022

2021

Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2021

Integrated Deduction (Dagstuhl Seminar 21371).

[BibT_eX]

[DOI]

Maria Paola Bonacina

Renate A. Schmidt

Dagstuhl Reports, 2021

CertiStr: A Certified String Solver (technical report).

[BibT_eX]

[DOI]

CoRR, 2021

Competition Report: CHC-COMP-21.

[BibT_eX]

[DOI]

Grigory Fedyukovich

Proceedings of the Proceedings 8th Workshop on Horn Clauses for Verification and Synthesis, 2021

A Theory of Heap for Constrained Horn Clauses (Extended Technical Report).

[BibT_eX]

[DOI]

CoRR, 2021

Towards String Support in JayHorn (Competition Contribution).

[BibT_eX]

[DOI]

Ali Shamakhi

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2021

Regular Model Checking Revisited.

[BibT_eX]

[DOI]

Proceedings of the Model Checking, Synthesis, and Learning, 2021

2020

Constraint-Based Contract Inference for Deductive Verification.

[BibT_eX]

[DOI]

Proceedings of the Deductive Software Verification: Future Perspectives, 2020

Probabilistic Bisimulation for Parameterized Systems (Technical Report).

[BibT_eX]

[DOI]

CoRR, 2020

String Constraints with Concatenation and Transducers Solved Efficiently (Technical Report).

[BibT_eX]

[DOI]

CoRR, 2020

Competition Report: CHC-COMP-20.

[BibT_eX]

[DOI]

Proceedings of the Proceedings 8th International Workshop on Verification and Program Transformation and 7th Workshop on Horn Clauses for Verification and Synthesis, 2020

Regular Model Checking Revisited (Technical Report).

[BibT_eX]

[DOI]

CoRR, 2020

Monadic Decomposition in Integer Linear Arithmetic (Technical Report).

[BibT_eX]

[DOI]

CoRR, 2020

Invited Talk: Solving String Constraints, Starting from the Beginning and from the End.

[BibT_eX]

[DOI]

Proceedings of the 18th International Workshop on Satisfiability Modulo Theories co-located with the 10th International Joint Conference on Automated Reasoning (IJCAR 2020), 2020

Abstract: Towards an SMT-LIB Theory of Heap.

[BibT_eX]

[DOI]

Proceedings of the 18th International Workshop on Satisfiability Modulo Theories co-located with the 10th International Joint Conference on Automated Reasoning (IJCAR 2020), 2020

Reasoning in the Theory of Heap: Satisfiability and Interpolation.

[BibT_eX]

[DOI]

Proceedings of the Logic-Based Program Synthesis and Transformation, 2020

Monadic Decomposition in Integer Linear Arithmetic.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

A Decision Procedure for Path Feasibility of String Manipulating Programs with Integer Data Type.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2020

2019

Decision procedures for path feasibility of string-manipulating programs with complex operations.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2019

Deduction Beyond Satisfiability (Dagstuhl Seminar 19371).

[BibT_eX]

[DOI]

Dagstuhl Reports, 2019

JayHorn: A Java Model Checker - (Competition Contribution).

[BibT_eX]

[DOI]

Temesghen Kahsai

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2019

JayHorn: a Java model checker.

[BibT_eX]

[DOI]

Proceedings of the 21st Workshop on Formal Techniques for Java-like Programs, 2019

Probabilistic Bisimulation for Parameterized Systems - (with Applications to Verifying Anonymous Protocols).

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 31st International Conference, 2019

On Strings in Software Model Checking.

[BibT_eX]

[DOI]

Ali Shamakhi

Proceedings of the Programming Languages and Systems - 17th Asian Symposium, 2019

2018

String constraints with concatenation and transducers solved efficiently.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2018

Automating regression verification of pointer programs by predicate abstraction.

[BibT_eX]

[DOI]

Vladimir Klebanov

Mattias Ulbrich

Formal Methods Syst. Des., 2018

Deciding and Interpolating Algebraic Data Types by Reduction (Technical Report).

[BibT_eX]

[DOI]

CoRR, 2018

The ELDARICA Horn Solver.

[BibT_eX]

[DOI]

Proceedings of the 2018 Formal Methods in Computer Aided Design, 2018

Bit-Vector Interpolation and Quantifier Elimination by Lazy Reduction.

[BibT_eX]

[DOI]

Proceedings of the 2018 Formal Methods in Computer Aided Design, 2018

Trau: SMT solver for string constraints.

[BibT_eX]

[DOI]

Proceedings of the 2018 Formal Methods in Computer Aided Design, 2018

Exploring Approximations for Floating-Point Arithmetic Using UppSAT.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 9th International Joint Conference, 2018

2017

An Approximation Framework for Solvers and Decision Procedures.

[BibT_eX]

[DOI]

J. Autom. Reason., 2017

Preface to special issue on satisfiability modulo theories.

[BibT_eX]

[DOI]

Alberto Griggio

Formal Methods Syst. Des., 2017

Fair Termination for Parameterized Probabilistic Concurrent Systems (Technical Report).

[BibT_eX]

[DOI]

CoRR, 2017

Learning to Prove Safety over Parameterised Concurrent Systems (Full Version).

[BibT_eX]

[DOI]

CoRR, 2017

Fair Termination for Parameterized Probabilistic Concurrent Systems.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2017

Deciding and Interpolating Algebraic Data Types by Reduction.

[BibT_eX]

[DOI]

Proceedings of the 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2017

Flatten and conquer: a framework for efficient analysis of string constraints.

[BibT_eX]

[DOI]

Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2017

Systematic Predicate Abstraction Using Variable Roles.

[BibT_eX]

[DOI]

Yulia Demyanova

Florian Zuleger

Proceedings of the NASA Formal Methods - 9th International Symposium, 2017

Quantified Heap Invariants for Object-Oriented Programs.

[BibT_eX]

[DOI]

Proceedings of the LPAR-21, 2017

Abduction by Non-Experts.

[BibT_eX]

[DOI]

Proceedings of the IWIL@LPAR 2017 Workshop and LPAR-21 Short Presentations, 2017

Learning to prove safety over parameterised concurrent systems.

[BibT_eX]

[DOI]

Proceedings of the 2017 Formal Methods in Computer Aided Design, 2017

2016

Proof Search with Taclets.

[BibT_eX]

[DOI]

Mattias Ulbrich

Proceedings of the Deductive Software Verification - The KeY Book, 2016

Liveness of Randomised Parameterised Systems under Arbitrary Schedulers (Technical Report).

[BibT_eX]

[DOI]

CoRR, 2016

Guiding Craig interpolation with domain-specific abstractions.

[BibT_eX]

[DOI]

Jérôme Leroux

Pavle Subotic

Acta Informatica, 2016

Regular Symmetry Patterns.

[BibT_eX]

[DOI]

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2016

Deciding Bit-Vector Formulas with mcSAT.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2016, 2016

Optimizing horn solvers for network repair.

[BibT_eX]

[DOI]

Proceedings of the 2016 Formal Methods in Computer-Aided Design, 2016

Liveness of Randomised Parameterised Systems under Arbitrary Schedulers.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 28th International Conference, 2016

JayHorn: A Framework for Verifying Java programs.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 28th International Conference, 2016

Characterization of Simulation by Probabilistic Testing.

[BibT_eX]

[DOI]

Wang Yi

Proceedings of the Theory and Practice of Formal Methods, 2016

2015

On recursion-free Horn clauses and Craig interpolation.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2015

Regular Symmetry Patterns (Technical Report).

[BibT_eX]

[DOI]

CoRR, 2015

Efficient Algorithms for Bounded Rigid E-unification.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2015

Automating Regression Verification.

[BibT_eX]

Proceedings of the Software Engineering & Management 2015, Multikonferenz der GI-Fachbereiche Softwaretechnik (SWT) und Wirtschaftsinformatik (WI), FA WI-MAW, 17. März, 2015

Conflict-Directed Graph Coverage.

[BibT_eX]

[DOI]

Daniel Schwartz-Narbonne

Proceedings of the NASA Formal Methods - 7th International Symposium, 2015

Bixie: Finding and Understanding Inconsistent Code.

[BibT_eX]

[DOI]

Tim McCarthy

Proceedings of the 37th IEEE/ACM International Conference on Software Engineering, 2015

Free Variables and Theories: Revisiting Rigid E-unification.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems - 10th International Symposium, 2015

Norn: An SMT Solver for String Constraints.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 27th International Conference, 2015

Theorem Proving with Bounded Rigid E-Unification.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-25, 2015

An Automatable Formal Semantics for IEEE-754 Floating-Point Arithmetic.

[BibT_eX]

[DOI]

Proceedings of the 22nd IEEE Symposium on Computer Arithmetic, 2015

2014

Horn Clauses for Communicating Timed Systems.

[BibT_eX]

[DOI]

Proceedings of the Proceedings First Workshop on Horn Clauses for Verification and Synthesis, 2014

The Gradual Verifier.

[BibT_eX]

[DOI]

Proceedings of the NASA Formal Methods - 6th International Symposium, NFM 2014, Houston, TX, USA, April 29, 2014

String Constraints for Verification.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 26th International Conference, 2014

Approximations for Model Construction.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 7th International Joint Conference, 2014

2013

Ranking function synthesis for bit-vector relations.

[BibT_eX]

[DOI]

Byron Cook

Formal Methods Syst. Des., 2013

The Relationship between Craig Interpolation and Recursion-Free Horn Clauses

[BibT_eX]

[DOI]

CoRR, 2013

Disjunctive Interpolants for Horn-Clause Verification (Extended Technical Report)

[BibT_eX]

[DOI]

CoRR, 2013

Classifying and Solving Horn Clauses for Verification.

[BibT_eX]

[DOI]

Proceedings of the Verified Software: Theories, Tools, Experiments, 2013

Joogie: from Java through Jimple to Boogie.

[BibT_eX]

[DOI]

Stephan Arlt

Proceedings of the 2nd ACM SIGPLAN International Workshop on State Of the Art in Java Program analysis, 2013

Exploring interpolants.

[BibT_eX]

[DOI]

Pavle Subotic

Proceedings of the Formal Methods in Computer-Aided Design, 2013

Disjunctive Interpolants for Horn-Clause Verification.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 25th International Conference, 2013

A Theory for Control-Flow Graph Exploration.

[BibT_eX]

[DOI]

Stephan Arlt

Proceedings of the Automated Technology for Verification and Analysis, 2013

2012

Craig Interpolation for the Integers: Results, Implementation, and Experiences.

[BibT_eX]

[DOI]

Proceedings of the IWIL 2012: The 9th International Workshop on the Implementation of Logics, 2012

E-Matching with Free Variables.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2012

A Verification Toolkit for Numerical Transition Systems - Tool Paper.

[BibT_eX]

[DOI]

Proceedings of the FM 2012: Formal Methods, 2012

Accelerating Interpolants.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2012

2011

An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic.

[BibT_eX]

[DOI]

J. Autom. Reason., 2011

Automatic analysis of DMA races using model checking and <i>k</i>-induction.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2011

Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic.

[BibT_eX]

[DOI]

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2011

Software Verification Using k-Induction.

[BibT_eX]

[DOI]

Leopold Haller

Proceedings of the Static Analysis - 18th International Symposium, 2011

SCRATCH: a tool for automatic analysis of dma races.

[BibT_eX]

[DOI]

Proceedings of the 16th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, 2011

Test-case generation for embedded simulink via formal concept analysis.

[BibT_eX]

[DOI]

Nannan He

Proceedings of the 48th Design Automation Conference, 2011

2010

Practical Aspects of Automated Deduction for Program Verification.

[BibT_eX]

[DOI]

Künstliche Intell., 2010

Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic (Extended Technical Report)

[BibT_eX]

[DOI]

CoRR, 2010

A Polymorphic Intermediate Verification Language: Design and Logical Encoding.

[BibT_eX]

[DOI]

K. Rustan M. Leino

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2010

Automatic Analysis of Scratch-Pad Memory Code for Heterogeneous Multicore Processors.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2010

Interpolating Quantifier-Free Presburger Arithmetic.

[BibT_eX]

[DOI]

Jérôme Leroux

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2010

Tightening Test Coverage Metrics: A Case Study in Equivalence Checking Using k-Induction.

[BibT_eX]

[DOI]

Nannan He

Proceedings of the Formal Methods for Components and Objects - 9th International Symposium, 2010

Program Verification via Craig Interpolation for Presburger Arithmetic with Arrays.

[BibT_eX]

[DOI]

Proceedings of the 6th International Verification Workshop, 2010

2009

Mutation-Based Test Case Generation for Simulink Models.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods for Components and Objects - 8th International Symposium, 2009

Real World Verification.

[BibT_eX]

[DOI]

André Platzer

Jan-David Quesel

Proceedings of the Automated Deduction, 2009

2008

Integration of a security type system into a program logic.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2008

Non-termination Checking for Imperative Programs.

[BibT_eX]

[DOI]

Helga Velroyen

Proceedings of the Tests and Proofs - 2nd International Conference, 2008

Integrating Verification and Testing of Object-Oriented Software.

[BibT_eX]

[DOI]

Proceedings of the Tests and Proofs - 2nd International Conference, 2008

A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2008

2007

Construction of Proofs.

[BibT_eX]

[DOI]

Proceedings of the Verification of Object-Oriented Software. The KeY Approach, 2007

Proving Programs Incorrect Using a Sequent Calculus for Java Dynamic Logic.

[BibT_eX]

[DOI]

Muhammad Ali Shah

Proceedings of the Tests and Proofs - 1st International Conference, 2007

A Sequent Calculus for Integer Arithmetic with Counterexample Generation.

[BibT_eX]

[DOI]

Proceedings of 4th International Verification Workshop in connection with CADE-21, 2007

The KeY system 1.0 (Deduction Component).

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2007

2006

Sequential, Parallel, and Quantified Updates of First-Order Structures.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2006

Verifying Object-Oriented Programs with KeY: A Tutorial.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods for Components and Objects, 5th International Symposium, 2006

2005

Verification of JCSP Programs.

[BibT_eX]

[DOI]

Proceedings of the 28th Communicating Process Architectures Conference, 2005

2004

Ensuring the Correctness of Lightweight Tactics for JavaCard Dynamic Logic.

[BibT_eX]

[DOI]

Richard Bubel

Andreas Roth