Understanding Counterexamples for Relational Properties with DIbugger
| Autor: | Benedikt Wagner, Pascal Zwick, Mihai Herda, Michael Kirsten, Etienne Brunner, Bernhard Beckert, Joana Plewnia, Ulla Scheler, Chiara Staudenmaier |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2019 |
| Předmět: |
FOS: Computer and information sciences
Property (philosophy) Computer Science - Cryptography and Security Computer science media_common.quotation_subject computer.software_genre lcsh:QA75.5-76.95 Computer Science - Software Engineering Software Software verification Relational properties media_common Computer Science - Programming Languages business.industry Programming language lcsh:Mathematics DATA processing & computer science Process (computing) lcsh:QA1-939 Software Engineering (cs.SE) Debugging lcsh:Electronic computers. Computer science ddc:004 business computer Cryptography and Security (cs.CR) Counterexample Programming Languages (cs.PL) |
| Zdroj: | Electronic Proceedings in Theoretical Computer Science, Vol 296, Iss Proc. HCVS/PERR 2019, Pp 6-13 (2019) HCVS/PERR@ETAPS |
| ISSN: | 2075-2180 |
| Popis: | Software verification is a tedious process that involves the analysis of multiple failed verification attempts, and adjustments of the program or specification. This is especially the case for complex requirements, e.g., regarding security or fairness, when one needs to compare multiple related runs of the same software. Verification tools often provide counterexamples consisting of program inputs when a proof attempt fails, however it is often not clear why the reported counterexample leads to a violation of the checked property. In this paper, we enhance this aspect of the software verification process by providing DIbugger, a tool for analyzing counterexamples of relational properties, allowing the user to debug multiple related programs simultaneously. In Proceedings HCVS/PERR 2019, arXiv:1907.03523 |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|