DROPS

Document

DOI: 10.4230/LIPIcs.CONCUR.2015.456

Unfolding-based Partial Order Reduction

Authors: César Rodríguez, Marcelo Sousa, Subodh Sharma, and Daniel Kroening

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)

Abstract

Partial order reduction (POR) and net unfoldings are two alternative methods to tackle state-space explosion caused by concurrency. In this paper, we propose the combination of both approaches in an effort to combine their strengths. We first define, for an abstract execution model, unfolding semantics parameterized over an arbitrary independence relation. Based on it, our main contribution is a novel stateless POR algorithm that explores at most one execution per Mazurkiewicz trace, and in general, can explore exponentially fewer, thus achieving a form of super-optimality. Furthermore, our unfolding-based POR copes with non-terminating executions and incorporates state caching. On benchmarks with busy-waits, among others, our experiments show a dramatic reduction in the number of executions when compared to a state-of-the-art DPOR.

Cite as

César Rodríguez, Marcelo Sousa, Subodh Sharma, and Daniel Kroening. Unfolding-based Partial Order Reduction. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 456-469, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{rodriguez_et_al:LIPIcs.CONCUR.2015.456,
  author =	{Rodr{\'\i}guez, C\'{e}sar and Sousa, Marcelo and Sharma, Subodh and Kroening, Daniel},
  title =	{{Unfolding-based Partial Order Reduction}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{456--469},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.456},
  URN =		{urn:nbn:de:0030-drops-53637},
  doi =		{10.4230/LIPIcs.CONCUR.2015.456},
  annote =	{Keywords: Partial order reduction, unfoldings, concurrency, model checking}
}

Document

DOI: 10.4230/DagRep.4.8.89

Decision Procedures and Abstract Interpretation (Dagstuhl Seminar 14351)

Authors: Daniel Kroening, Thomas W. Reps, Sanjit A. Seshia, and Aditya Thakur

Published in: Dagstuhl Reports, Volume 4, Issue 8 (2015)

Abstract

This report documents the program and the outcomes of Dagstuhl Seminar 14351 "Decision Procedures and Abstract Interpretation". The seminar brought together practitioners and reseachers in abstract interpretation and decision procedures. The meeting highlighted the connections between the two disciplines, and created new links between the two research communities. Joint activities were also conducted with the participants of Dagstuhl Seminar 14352 "Next Generation Static Software Analysis Tools", which was held concurrently.

Cite as

Daniel Kroening, Thomas W. Reps, Sanjit A. Seshia, and Aditya Thakur. Decision Procedures and Abstract Interpretation (Dagstuhl Seminar 14351). In Dagstuhl Reports, Volume 4, Issue 8, pp. 89-106, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@Article{kroening_et_al:DagRep.4.8.89,
  author =	{Kroening, Daniel and Reps, Thomas W. and Seshia, Sanjit A. and Thakur, Aditya},
  title =	{{Decision Procedures and Abstract Interpretation (Dagstuhl Seminar 14351)}},
  pages =	{89--106},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2014},
  volume =	{4},
  number =	{8},
  editor =	{Kroening, Daniel and Reps, Thomas W. and Seshia, Sanjit A. and Thakur, Aditya},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.4.8.89},
  URN =		{urn:nbn:de:0030-drops-48007},
  doi =		{10.4230/DagRep.4.8.89},
  annote =	{Keywords: Program analysis, Abstract interpretation, Abstract domain, Fixed-point finding, Satisfiability checking, Satisfiability modulo theories, Decision pro}
}

Document

DOI: 10.4230/DagRep.4.8.107

Next Generation Static Software Analysis Tools (Dagstuhl Seminar 14352)

Authors: Patrick Cousot, Daniel Kroening, and Carsten Sinz

Published in: Dagstuhl Reports, Volume 4, Issue 8 (2015)

Abstract

There has been tremendous progress in static software analysis over the last years with, for example, refined abstract interpretation methods, the advent of fast decision procedures like SAT and SMT solvers, new approaches like software (bounded) model checking or CEGAR, or new problem encodings. We are now close to integrating these techniques into every programmer's toolbox. The aim of the seminar was to bring together developers of software analysis tools and algorithms, including researchers working on the underlying decision procedures (e.g., SMT solvers), and people who are interested in applying these techniques (e.g. in the automotive or avionics industry). The seminar offered the unique chance, by assembling the leading experts in these areas, to make a big step ahead towards new, more powerful tools for static software analysis. Current (academic) tools still suffer from some shortcomings: - Tools are not yet robust enough or support only a subset of a programming language's features. - Scalability to large software packages is not yet sufficient. - There is a lack of standardized property specification and environment modeling constructs, which makes exchange of analysis results more complicated than necessary. - Differing interpretations of programming language semantics by different tools lead to limited trust in analysis results. - Moreover, a comprehensive benchmark collection to compare and evaluate tools is missing. Besides these application-oriented questions, further, more fundamental questions have also been topics of the seminar: - What are the right logics for program verification, bug finding and software analysis? - How can we handle universal quantification? And how to model main memory and complex data structures? - Which decision procedures are most suitable for static software analysis? How can different procedures be combined? Which optimizations to general-purpose decision procedures (SAT/SMT/QBF) are possible in the context of software analysis?

Cite as

Patrick Cousot, Daniel Kroening, and Carsten Sinz. Next Generation Static Software Analysis Tools (Dagstuhl Seminar 14352). In Dagstuhl Reports, Volume 4, Issue 8, pp. 107-125, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@Article{cousot_et_al:DagRep.4.8.107,
  author =	{Cousot, Patrick and Kroening, Daniel and Sinz, Carsten},
  title =	{{Next Generation Static Software Analysis Tools (Dagstuhl Seminar 14352)}},
  pages =	{107--125},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2014},
  volume =	{4},
  number =	{8},
  editor =	{Cousot, Patrick and Kroening, Daniel and Sinz, Carsten},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.4.8.107},
  URN =		{urn:nbn:de:0030-drops-48203},
  doi =		{10.4230/DagRep.4.8.107},
  annote =	{Keywords: Software quality, Bug finding, Verification, Decision procedures, SMT/SAT solvers}
}

3 Search Results for "Kroening, Daniel"

Unfolding-based Partial Order Reduction

Abstract

Cite as

Decision Procedures and Abstract Interpretation (Dagstuhl Seminar 14351)

Abstract

Cite as

Next Generation Static Software Analysis Tools (Dagstuhl Seminar 14352)

Abstract

Cite as

Thanks for your feedback!

Could not send message