Jochen Hoenicke

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

Proof Tree Preserving Sequence Interpolation of Quantified Formulas in the Theory of Equality.

[BibT_eX]

[DOI]

Elisabeth Henkel

Proceedings of the 19th International Workshop on Satisfiability Modulo Theories co-located with 33rd International Conference on Computer Aided Verification(CAV 2021), 2021

Separating Map Variables in a Logic-Based Intermediate Verification Language.

[BibT_eX]

[DOI]

Proceedings of the Networked Systems - 9th International Conference, 2021

2019

Ultimate TreeAutomizer (CHC-COMP Tool Description).

[BibT_eX]

[DOI]

Proceedings of the Sixth Workshop on Horn Clauses for Verification and Synthesis and Third Workshop on Program Equivalence and Relational Reasoning, 2019

Interpolation and the Array Property Fragment.

[BibT_eX]

[DOI]

CoRR, 2019

Different Maps for Different Uses. A Program Transformation for Intermediate Verification Languages.

[BibT_eX]

[DOI]

CoRR, 2019

Solving and Interpolating Constant Arrays Based on Weak Equivalences.

[BibT_eX]

[DOI]

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

Scalable Analysis of Real-Time Requirements.

[BibT_eX]

[DOI]

Proceedings of the 27th IEEE International Requirements Engineering Conference, 2019

2018

Reducing liveness to safety in first-order logic.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2018

A Tree-Based Approach to Data Flow Proofs.

[BibT_eX]

[DOI]

Alexander Nutz

Proceedings of the Verified Software. Theories, Tools, and Experiments, 2018

The Map Equality Domain.

[BibT_eX]

[DOI]

Proceedings of the Verified Software. Theories, Tools, and Experiments, 2018

Ultimate Automizer and the Search for Perfect Interpolants - (Competition Contribution).

[BibT_eX]

[DOI]

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

Ultimate Taipan with Dynamic Block Encoding - (Competition Contribution).

[BibT_eX]

[DOI]

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

Efficient Interpolation for the Theory of Arrays.

[BibT_eX]

[DOI]

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

2017

Thread modularity at many levels: a pearl in compositional verification.

[BibT_eX]

[DOI]

Rupak Majumdar

Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017

2016

Proof Tree Preserving Tree Interpolation.

[BibT_eX]

[DOI]

J. Autom. Reason., 2016

2015

Automated Program Verification.

[BibT_eX]

[DOI]

Proceedings of the Language and Automata Theory and Applications, 2015

Weakly Equivalent Arrays.

[BibT_eX]

[DOI]

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

Cutting the Mix.

[BibT_eX]

[DOI]

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

Fairness for Infinitary Control.

[BibT_eX]

[DOI]

Proceedings of the Correct System Design, 2015

2014

Ultimate Automizer with Unsatisfiable Cores - (Competition Contribution).

[BibT_eX]

[DOI]

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

Ultimate Kojak - (Competition Contribution).

[BibT_eX]

[DOI]

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

Termination Analysis by Learning Terminating Programs.

[BibT_eX]

[DOI]

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

2013

Ultimate Automizer with SMTInterpol - (Competition Contribution).

[BibT_eX]

[DOI]

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

Proof Tree Preserving Interpolation.

[BibT_eX]

[DOI]

Alexander Nutz

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

Software Model Checking for People Who Love Automata.

[BibT_eX]

[DOI]

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

Linear Ranking for Linear Lasso Programs.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2013

2012

Automotive behavioral requirements expressed in a specification pattern system: a case study at BOSCH.

[BibT_eX]

[DOI]

Requir. Eng., 2012

Towards Bounded Infeasible Code Detection

[BibT_eX]

[DOI]

Martin Schäf

CoRR, 2012

Formalization and Analysis of Real-Time Requirements: A Feasibility Study at BOSCH.

[BibT_eX]

[DOI]

Amalinda Post

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

Splitting via Interpolants.

[BibT_eX]

[DOI]

Evren Ermis

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

SMTInterpol: An Interpolating SMT Solver.

[BibT_eX]

[DOI]

Alexander Nutz

Proceedings of the Model Checking Software - 19th International Workshop, 2012

2011

Vacuous real-time requirements.

[BibT_eX]

[DOI]

Amalinda Post

Proceedings of the RE 2011, 19th IEEE International Requirements Engineering Conference, Trento, Italy, August 29 2011, 2011

rt-Inconsistency: A New Property for Real-Time Requirements.

[BibT_eX]

[DOI]

Amalinda Post

Proceedings of the Fundamental Approaches to Software Engineering, 2011

2010

Doomed program points.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2010

Fairness for Dynamic Control.

[BibT_eX]

[DOI]

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

Nested interpolants.

[BibT_eX]

[DOI]

Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2010

Instantiation-Based Interpolation for Quantified Formulae.

[BibT_eX]

[DOI]

Proceedings of the Decision Procedures in Software, Hardware and Bioware, 18.04., 2010

Kleene, Rabin, and Scott Are Available.

[BibT_eX]

[DOI]

Roland Meyer

Proceedings of the CONCUR 2010 - Concurrency Theory, 21th International Conference, 2010

2009

Refinement of Trace Abstraction.

[BibT_eX]

[DOI]

Proceedings of the Static Analysis, 16th International Symposium, 2009

It's Doomed; We Can Prove It.

[BibT_eX]

[DOI]

Proceedings of the FM 2009: Formal Methods, 2009

2008

Model checking Duration Calculus: a practical approach.

[BibT_eX]

[DOI]

Formal Aspects Comput., 2008

2006

Combination of processes, data, and time.

[BibT_eX]

[DOI]

PhD thesis, 2006

2005

Model-Checking of Specifications Integrating Processes, Data and Time.

[BibT_eX]

[DOI]

Patrick Maier

Proceedings of the FM 2005: Formal Methods, 2005

2002

CSP-OZ-DC: A Combination of Specification Techniques for Processes, Data and Time.

[BibT_eX]

Nord. J. Comput., 2002

Combining Specification Techniques for Processes, Data and Time.

[BibT_eX]

[DOI]