Program correctness techniques aim to prove the absence of bugs, but can yield false alarms because they tend to over-approximate program semantics. Vice versa, program incorrectness methods are aimed to detect true bugs, without false alarms, but cannot be used to prove correctness, because they under-approximate program semantics. In this invited talk we will overview our ongoing research on the use of the abstract interpretation framework to combine under- and over-approximation in the same analysis and distill a logic for program correctness and incorrectness.
@InProceedings{bruni:LIPIcs.CALCO.2023.2, author = {Bruni, Roberto}, title = {{Local Completeness for Program Correctness and Incorrectness}}, booktitle = {10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)}, pages = {2:1--2:2}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-287-7}, ISSN = {1868-8969}, year = {2023}, volume = {270}, editor = {Baldan, Paolo and de Paiva, Valeria}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.2}, URN = {urn:nbn:de:0030-drops-187993}, doi = {10.4230/LIPIcs.CALCO.2023.2}, annote = {Keywords: Program analysis, program verification, Hoare logic, incorrectness logic, abstract interpretation, local completeness} }
Feedback for Dagstuhl Publishing