Radu Iosif

CoRR, 2024

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

[BibT_eX]

[DOI]

Lucas Bueri

CoRR, 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

Verification of component-based systems with recursive architectures.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 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

Expressiveness Results for an Inductive Logic of Separated Relations.

[BibT_eX]

[DOI]

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

2022

Reasoning about distributed reconfigurable systems.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2022

Entailment is Undecidable for Symbolic Heap Separation Logic Formulæ with Non-Established Inductive Rules.

[BibT_eX]

[DOI]

Inf. Process. Lett., 2022

On the Expressiveness of a Logic of Separated Relations.

[BibT_eX]

[DOI]

CoRR, 2022

On an Invariance Problem for Parameterized Concurrent Systems.

[BibT_eX]

[DOI]

Lucas Bueri

Proceedings of the 33rd International Conference on Concurrency Theory, 2022

Decision Problems in a Logic for Reasoning About Reconfigurable Distributed Systems.

[BibT_eX]

[DOI]

Lucas Bueri

Proceedings of the Automated Reasoning - 11th International Joint Conference, 2022

2021

Checking deadlock-freedom of parametric component-based systems.

[BibT_eX]

[DOI]

J. Log. Algebraic Methods Program., 2021

Local Reasoning about Parameterized Reconfigurable Distributed Systems.

[BibT_eX]

[DOI]

CoRR, 2021

Specification and Safety Verification of Parametric Hierarchical Distributed Systems.

[BibT_eX]

[DOI]

Proceedings of the Formal Aspects of Component Software - 17th International Conference, 2021

Decidable Entailments in Separation Logic with Inductive Definitions: Beyond Establishment.

[BibT_eX]

[DOI]

Proceedings of the 29th EACSL Annual Conference on Computer Science Logic, 2021

Unifying Decidable Entailments in Separation Logic with Inductive Definitions.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE 28, 2021

2020

The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2020

Abstraction refinement and antichains for trace inclusion of infinite state systems.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2020

Checking Entailment Between Separation Logic Symbolic Heaps: Beyond Connected and Established Systems.

[BibT_eX]

[DOI]

CoRR, 2020

Verifying Safety Properties of Inductively Defined Parameterized Systems.

[BibT_eX]

[DOI]

CoRR, 2020

Decidable Entailments in Separation Logic with Inductive Definitions: Beyond Established Systems.

[BibT_eX]

[DOI]

CoRR, 2020

Structural Invariants for the Verification of Systems with Parameterized Architectures.

[BibT_eX]

[DOI]

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

Entailment Checking in Separation Logic with Inductive Definitions is 2-EXPTIME hard.

[BibT_eX]

[DOI]

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

2019

Local Reasoning about Parametric and Reconfigurable Component-based Systems.

[BibT_eX]

[DOI]

CoRR, 2019

Structural Invariants for Parametric Verification of Systems with Almost Linear Architectures.

[BibT_eX]

[DOI]

CoRR, 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

Prenex Separation Logic with One Selector Field.

[BibT_eX]

[DOI]

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

The Bernays-Schönfinkel-Ramsey Class of Separation Logic on Arbitrary Domains.

[BibT_eX]

[DOI]

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

Alternating Automata Modulo First Order Theories.

[BibT_eX]

[DOI]

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

2018

An Entailment Checker for Separation Logic with Inductive Definitions.

[BibT_eX]

[DOI]

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

First Order Alternation.

[BibT_eX]

[DOI]

CoRR, 2018

The Complexity of Prenex Separation Logic with One Selector.

[BibT_eX]

[DOI]

CoRR, 2018

On the Expressive Completeness of Bernays-Schönfinkel-Ramsey Separation Logic.

[BibT_eX]

[DOI]

CoRR, 2018

Abstraction Refinement for Emptiness Checking of Alternating Data Automata.

[BibT_eX]

[DOI]

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

Program Verification with Separation Logic.

[BibT_eX]

[DOI]

Proceedings of the Model Checking Software - 25th International Symposium, 2018

A Complete Cyclic Proof System for Inductive Entailments in First Order Logic.

[BibT_eX]

[DOI]

Proceedings of the LPAR-22. 22nd International Conference on Logic for Programming, 2018

2017

Underapproximation of procedure summaries for integer programs.

[BibT_eX]

[DOI]

Pierre Ganty

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

The Impact of Alternation.

[BibT_eX]

[DOI]

CoRR, 2017

Complete Cyclic Proof Systems for Inductive Entailments.

[BibT_eX]

[DOI]

CoRR, 2017

Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic.

[BibT_eX]

[DOI]

Andrew Reynolds

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

2016

Reasoning in the Bernays-Schoenfinkel-Ramsey Fragment of Separation Logic.

[BibT_eX]

[DOI]

Andrew Reynolds

CoRR, 2016

A Decision Procedure for Separation Logic in SMT.

[BibT_eX]

[DOI]

Andrew Reynolds

Tim King

CoRR, 2016

Abstraction Refinement and Antichains for Trace Inclusion of Infinite State Systems.

[BibT_eX]

[DOI]

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

A Decision Procedure for Separation Logic in SMT.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2016

How Hard is It to Verify Flat Affine Counter Systems with the Finite Monoid Property?

[BibT_eX]

[DOI]

Arnaud Sangnier

Proceedings of the Automated Technology for Verification and Analysis, 2016

2015

Interprocedural Reachability for Flat Integer Programs.

[BibT_eX]

[DOI]

Pierre Ganty

Proceedings of the Fundamentals of Computation Theory - 20th International Symposium, 2015

2014

Deciding Conditional Termination

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2014

Abstraction Refinement for Trace Inclusion of Data Automata.

[BibT_eX]

[DOI]

CoRR, 2014

Generating Bounded Languages Using Bounded Control Sets.

[BibT_eX]

[DOI]

Pierre Ganty

CoRR, 2014

Safety Problems Are NP-complete for Flat Integer Programs with Octagonal Loops.

[BibT_eX]

[DOI]

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

Deciding Entailments in Inductive Separation Logic with Tree Automata.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2014

2013

Automata-Based Termination Proofs.

[BibT_eX]

[DOI]

Comput. Informatics, 2013

The Tree Width of Separation Logic with Recursive Definitions.

[BibT_eX]

[DOI]

Jirí Simácek

Proceedings of the Automated Deduction - CADE-24, 2013

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

Programs with lists are counter automata.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2011

2010

Quantitative Separation Logic and Programs with Lists.

[BibT_eX]

[DOI]

Swann Perarnau

J. Autom. Reason., 2010

Automata-based verification of programs with tree updates.

[BibT_eX]

[DOI]

Peter Habermehl

Acta Informatica, 2010

Fast Acceleration of Ultimately Periodic Relations.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 22nd International Conference, 2010

Tool Demonstration of the FLATA Counter Automata Toolset.

[BibT_eX]

[DOI]

Proceedings of the Second International Workshop on Invariant Generation, 2010

2009

Flat Parametric Counter Automata.

[BibT_eX]

[DOI]

Yassine Lakhnech

Fundam. Informaticae, 2009

Iterating Octagons.

[BibT_eX]

[DOI]

Codruta Gîrlea

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

Automatic Verification of Integer Array Programs.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 21st International Conference, 2009

2008

A Logic of Singly Indexed Arrays.

[BibT_eX]

[DOI]

Peter Habermehl

Proceedings of the Logic for Programming, 2008

What Else Is Decidable about Integer Arrays?.

[BibT_eX]

[DOI]

Peter Habermehl

Proceedings of the Foundations of Software Science and Computational Structures, 2008

2007

On Flat Programs with Lists.

[BibT_eX]

[DOI]

Proceedings of the Verification, 2007

Proving Termination of Tree Manipulating Programs.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2007

2005

Translating Java for Multiple Model Checkers: The Bandera Back-End.

[BibT_eX]

[DOI]

Matthew B. Dwyer

John Hatcliff

Formal Methods Syst. Des., 2005

On Decidability Within the Arithmetic of Addition and Divisibility.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Science and Computational Structures, 2005

2004

Symmetry reductions for model checking of concurrent dynamic software.

[BibT_eX]

[DOI]

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

On Logics of Aliasing.

[BibT_eX]

[DOI]

Yassine Lakhnech

Proceedings of the Static Analysis, 11th International Symposium, 2004

2003

Temporal logic properties of Java objects.

[BibT_eX]

[DOI]

J. Syst. Softw., 2003

Space-Reduction Strategies for Model Checking Dynamic Software.

[BibT_eX]

[DOI]

Proceedings of the 2003 Workshop on Software Model Checking, 2003

Storeless semantics and alias logic.

[BibT_eX]

[DOI]

Yassine Lakhnech

Proceedings of the 2003 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation, 2003

2002

Symmetry Reduction Criteria for Software Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Model Checking of Software, 2002

2001

Exploiting Heap Symmetries in Explicit-State Model Checking of Software.

[BibT_eX]

[DOI]

Proceedings of the 16th IEEE International Conference on Automated Software Engineering (ASE 2001), 2001

2000

Using Garbage Collection in Model Checking.

[BibT_eX]

[DOI]

Proceedings of the SPIN Model Checking and Software Verification, 7th International SPIN Workshop, Stanford, CA, USA, August 30, 2000

Formal verification applied to Java concurrent software.

[BibT_eX]

[DOI]

Proceedings of the 22nd International Conference on on Software Engineering, 2000

1999

A Deadlock Detection Tool for Concurrent Java Programs.

[BibT_eX]

[DOI]

Claudio Demartini

Softw. Pract. Exp., 1999

dSPIN: A Dynamic Extension of SPIN.

[BibT_eX]

[DOI]

Claudio Demartini