Understanding counterexamples for relational properties with \textit{DIbugger}

MaRDI QIDQ5016380zbMATH OpenFDO

Authors Mihai Herda, Michael Kirsten, Etienne Brunner, Joana Plewnia, Ulla Scheler, Chiara Staudenmaier, Benedikt Wagner, Pascal Zwick, Bernhard Beckert

Publication date 13 December 2021

Full work available at URL https://arxiv.org/abs/1907.03996, http://eptcs.web.cse.unsw.edu.au/paper.cgi?HCVSPERR2019.4

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Understanding counterexamples with \texttt{explain}
• Debugging of concurrent systems using counterexample analysis
• Efficient debugging in a formal verification environment
• FocusCheck: A tool for model checking and debugging sequential C programs
• A framework for counterexample generation and exploration

Cites work

• Relational program reasoning using compiler IR
• Understanding counterexamples with \texttt{explain}

Cited in

(2)

• How helpers hasten h-relations
• Understanding counterexamples with \texttt{explain}

This page was built for publication: Understanding counterexamples for relational properties with \textit{DIbugger}

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5016380)