Florian Zuleger

CoRR, 2024

Deciding Boolean Separation Logic via Small Models (Technical Report).

[BibT_eX]

[DOI]

CoRR, 2024

Effective MSO-Definability for Tree-width Bounded Models of an Inductive Separation Logic of Relations.

[BibT_eX]

[DOI]

Lucas Bueri

CoRR, 2024

Deciding Boolean Separation Logic via Small Models.

[BibT_eX]

[DOI]

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

Tree-Verifiable Graph Grammars.

[BibT_eX]

[DOI]

Mark Chimes

Proceedings of the LPAR 2024: Proceedings of 25th Conference on Logic for Programming, 2024

2023

A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions.

[BibT_eX]

[DOI]

Christoph Matheja

Jens Pagel

ACM Trans. Comput. Log., January, 2023

The Treewidth Boundedness Problem for an Inductive Separation Logic of Relations.

[BibT_eX]

[DOI]

CoRR, 2023

Characterizations of Definable Context-Free Graphs.

[BibT_eX]

[DOI]

CoRR, 2023

Parameterized Model-checking of Discrete-Timed Networks and Symmetric-Broadcast Systems.

[BibT_eX]

[DOI]

CoRR, 2023

Sound One-Phase Shape Analysis with Biabduction.

[BibT_eX]

[DOI]

CoRR, 2023

A Formalization of Heisenbugs and Their Causes.

[BibT_eX]

[DOI]

Sarah Sallinger

Proceedings of the Software Engineering and Formal Methods - 21st International Conference, 2023

Embedding Intuitionistic into Classical Logic.

[BibT_eX]

[DOI]

Alexander Pluska

Proceedings of the LPAR 2023: Proceedings of 24th International Conference on Logic for Programming, 2023

Stochastic Best-Effort Strategies for Borel Goals.

[BibT_eX]

[DOI]

Proceedings of the 38th Annual ACM/IEEE Symposium on Logic in Computer Science, 2023

Expressiveness Results for an Inductive Logic of Separated Relations.

[BibT_eX]

[DOI]

Proceedings of the 34th International Conference on Concurrency Theory, 2023

Algorithmenerkennung und Programmreparatur mittels Dynamischer Programmanalyse.

[BibT_eX]

[DOI]

Proceedings of the Sixth Workshop "Automatische Bewertung von Programmieraufgaben", 2023

2022

Type-based analysis of logarithmic amortised complexity.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., June, 2022

Strong-separation Logic.

[BibT_eX]

[DOI]

Jens Pagel

ACM Trans. Program. Lang. Syst., 2022

Verifying safety of synchronous fault-tolerant algorithms by bounded model checking.

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 2022

Low-Level Bi-Abduction (Artifact).

[BibT_eX]

[DOI]

Dagstuhl Artifacts Ser., 2022

On the Expressiveness of a Logic of Separated Relations.

[BibT_eX]

[DOI]

CoRR, 2022

Verification of agent navigation in partially-known environments.

[BibT_eX]

[DOI]

Artif. Intell., 2022

Beyond Strong-Cyclic: Doing Your Best in Stochastic Environments.

[BibT_eX]

[DOI]

Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, 2022

Low-Level Bi-Abduction.

[BibT_eX]

[DOI]

Proceedings of the 36th European Conference on Object-Oriented Programming, 2022

Automated Expected Amortised Cost Analysis of Probabilistic Data Structures.

[BibT_eX]

[DOI]

Lorenz Leutgeb

Georg Moser

Proceedings of the Computer Aided Verification - 34th International Conference, 2022

2021

Rely-guarantee bound analysis of parameterized concurrent shared-memory programs.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2021

Eliminating Message Counters in Synchronous Threshold Automata.

[BibT_eX]

[DOI]

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

Bounded Model Checking of Speculative Non-Interference.

[BibT_eX]

[DOI]

Emmanuel Pescosta

Proceedings of the IEEE/ACM International Conference On Computer Aided Design, 2021

ATLAS: Automated Amortised Complexity Analysis of Self-adjusting Data Structures.

[BibT_eX]

[DOI]

Lorenz Leutgeb

Georg Moser

Proceedings of the Computer Aided Verification - 33rd International Conference, 2021

2020

Complete Entailment Checking for Separation Logic with Inductive Definitions.

[BibT_eX]

[DOI]

Jens Pagel

Christoph Matheja

CoRR, 2020

Multi-linear Strategy Extraction for QBF Expansion Proofs via Local Soundness.

[BibT_eX]

[DOI]

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

Beyond Symbolic Heaps: Deciding Separation Logic With Inductive Definitions.

[BibT_eX]

[DOI]

Jens Katelaan

Proceedings of the LPAR 2020: 23rd International Conference on Logic for Programming, 2020

The Polynomial Complexity of Vector Addition Systems with States.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Science and Computation Structures, 2020

Thread-modular Counter Abstraction for Parameterized Program Safety.

[BibT_eX]

[DOI]

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

Eliminating Message Counters in Threshold Automata.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2020

2019

SL-COMP: Competition of Solvers for Separation Logic.

[BibT_eX]

[DOI]

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

Effective Entailment Checking for Separation Logic with Inductive Definitions.

[BibT_eX]

[DOI]

Jens Katelaan

Christoph Matheja

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

2018

Monadic refinements for relational cost analysis.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2018

From Shapes to Amortized Complexity.

[BibT_eX]

[DOI]

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

Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction.

[BibT_eX]

[DOI]

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

Inductive Termination Proofs with Transition Invariants and Their Relationship to the Size-Change Abstraction.

[BibT_eX]

[DOI]

Proceedings of the Static Analysis - 25th International Symposium, 2018

Automated clustering and program repair for introductory programming assignments.

[BibT_eX]

[DOI]

Sumit Gulwani

Ivan Radicek

Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2018

Harrsh: A Tool for Unied Reasoning about Symbolic-Heap Separation Logic.

[BibT_eX]

[DOI]

Proceedings of the LPAR-22 Workshop and Short Paper Proceedings, 2018

Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS.

[BibT_eX]

[DOI]

Tomás Brázdil

Krishnendu Chatterjee

Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 2018

Rely-Guarantee Reasoning for Automated Bound Analysis of Lock-Free Algorithms.

[BibT_eX]

[DOI]

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

Using Loop Bound Analysis For Invariant Generation.

[BibT_eX]

[DOI]

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

2017

Complexity and Resource Bound Analysis of Imperative Programs Using Difference Constraints.

[BibT_eX]

[DOI]

J. Autom. Reason., 2017

Empirical software metrics for benchmarking of verification tools.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2017

Resource Bound Analysis (Dagstuhl Seminar 17291).

[BibT_eX]

[DOI]

Dagstuhl Reports, 2017

Ranking Functions for Vector Addition Systems.

[BibT_eX]

[DOI]

CoRR, 2017

Systematic Predicate Abstraction Using Variable Roles.

[BibT_eX]

[DOI]

Yulia Demyanova

Philipp Rümmer

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

On the Automated Verification of Web Applications with Embedded SQL.

[BibT_eX]

[DOI]

Proceedings of the 20th International Conference on Database Theory, 2017

Automata and Program Analysis.

[BibT_eX]

[DOI]

Thomas Colcombet

Laure Daviaud

Proceedings of the Fundamentals of Computation Theory - 21st International Symposium, 2017

Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2017

2016

Feedback generation for performance problems in introductory programming assignments.

[BibT_eX]

[DOI]

Ivan Radicek

Sumit Gulwani

Proceedings of the Software Engineering 2016, 2016

A simple and scalable static analysis for bound analysis and amortized complexity analysis.

[BibT_eX]

[DOI]

Proceedings of the Software Engineering 2016, 2016

Prompt Alternating-Time Epistemic Logics.

[BibT_eX]

[DOI]

Proceedings of the Principles of Knowledge Representation and Reasoning: Proceedings of the Fifteenth International Conference, 2016

Monadic Second Order Finite Satisfiability and Unbounded Tree-Width.

[BibT_eX]

[DOI]

Tomer Kotek

Proceedings of the 25th EACSL Annual Conference on Computer Science Logic, 2016

Automatic Verification of Multi-Agent Systems in Parameterised Grid-Environments.

[BibT_eX]

[DOI]

Proceedings of the 2016 International Conference on Autonomous Agents & Multiagent Systems, 2016

2015

Loop Patterns in C Programs.

[BibT_eX]

[DOI]

Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2015

Verification of Asynchronous Mobile-Robots in Partially-Known Environments.

[BibT_eX]

[DOI]

Proceedings of the PRIMA 2015: Principles and Practice of Multi-Agent Systems, 2015

On the Expressive Power of Communication Primitives in Parameterised Systems.

[BibT_eX]

[DOI]

Benjamin Aminof

Sasha Rubin

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

Extending ALCQIO with Trees.

[BibT_eX]

[DOI]

Proceedings of the 30th Annual ACM/IEEE Symposium on Logic in Computer Science, 2015

Liveness of Parameterized Timed Networks.

[BibT_eX]

[DOI]

Proceedings of the Automata, Languages, and Programming - 42nd International Colloquium, 2015

Difference Constraints: An adequate Abstraction for Complexity Analysis of Imperative Programs.

[BibT_eX]

[DOI]

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

Asymptotically Precise Ranking Functions for Deterministic Size-Change Systems.

[BibT_eX]

[DOI]

Proceedings of the Computer Science - Theory and Applications, 2015

2014

Extending ALCQIO with reachability.

[BibT_eX]

[DOI]

CoRR, 2014

Size-Change Abstraction and Max-Plus Automata.

[BibT_eX]

[DOI]

Thomas Colcombet

Laure Daviaud

Proceedings of the Mathematical Foundations of Computer Science 2014, 2014

Shape and Content - A Database-Theoretic Perspective on the Analysis of Data Structures.

[BibT_eX]

[DOI]

Proceedings of the Integrated Formal Methods - 11th International Conference, 2014

Towards a Description Logic for Program Analysis: Extending ALCQIO with Reachability.

[BibT_eX]

[DOI]

Proceedings of the Informal Proceedings of the 27th International Workshop on Description Logics, 2014

Shape and Content: Incorporating Domain Knowledge into Shape Analysis.

[BibT_eX]

[DOI]

Proceedings of the Informal Proceedings of the 27th International Workshop on Description Logics, 2014

2013

Ramsey vs. Lexicographic Termination Proving.

[BibT_eX]

[DOI]

Byron Cook

Abigail See

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

On the concept of variable roles and its use in software analysis.

[BibT_eX]

[DOI]

Yulia Demyanova

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

2012

Bound Analysis of Imperative Programs with the Size-change Abstraction (extended version)

[BibT_eX]

[DOI]

CoRR, 2012

2011

Bound Analysis of Imperative Programs with the Size-Change Abstraction.

[BibT_eX]

[DOI]

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

2010

The reachability-bound problem.

[BibT_eX]

[DOI]

Sumit Gulwani

Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, 2010

LOOPUS - A Tool for Computing Loop Bounds for C Programs.

[BibT_eX]

[DOI]

Proceedings of the Second International Workshop on Invariant Generation, 2010

2009

An Abstract Interpretation-Based Framework for Control Flow Reconstruction from Binaries.

[BibT_eX]

[DOI]

Johannes Kinder