The paper, titled "Unsatisfiability Proofs for Horn Solving", was awarded in the category "Papers related to the systematic and rigorous engineering of software systems".
The work is the result of a collaboration between Martin Blicha, Researcher at the Formal Verification Lab at USI led by Professor Natasha Sharygina, and Rodrigo Otoni, Researcher at the Software System Lab at USI led by Professor Eugster. Matias Barandiaran Rivera, Jan Kofron , Professor Patrick Eugster and Professor Natasha Sharygina also collaborated on the project.
The research group’s study starts from the observation that many verification tools currently rely on logic solvers as backend reasoning engines. Despite playing such a pivotal role, bugs are not uncommon in the complex codebases of these solvers. Validating their results is thus critical, with correctness witnesses often being used for this end. Output validation for constrained Horn clauses (CHC) solvers is not a well explored topic though, especially in regards to unsatisfiability results. This is a significant issue, given that CHC solvers are being increasingly employed in verification tooling. To address this problem, the researchers propose an approach to validate CHC unsatisfiability results based on independently checkable proofs. The proposed approach is generic in regards to the solving algorithm, preprocessing steps, and exact proof format used, and works by first producing a coarse-grained proof during solving and then instantiating it into a suitable proof format by adding missing details, at which point the instantiated proof can be checked by an independent proof checker. A state-of-the-art CHC solver has been implemented to generate proofs in the Alethe format and performed a large-scale evaluation. The results obtained indicate that proofs can be produced with minimal overhead, can be efficiently checked, and have tractable sizes.
TACAS is a forum for researchers, developers and users interested in rigorously based tools and algorithms for the construction and analysis of systems. The conference aims to bridge the gaps between different communities with this common interest and to support them in their quest to improve the utility, reliability, flexibility and efficiency of tools and algorithms for building systems. The TACAS conference is a founding member of ETAPS. Its roots date back to 1995, when it was first held in Aalborg, Denmark. Since then, the TACAS proceedings have been published in the LNCS series by Springer-Verlag. ETAPS is a confederation of several conferences, each with its own programme committee and steering committee.
ETAPS is the most important and visible annual European event related to software science. Overall, more than 500 researchers participate each year. The EASST Best Paper Award is given by a selected committee, which decides the winner of the award each year.
You can read the paper at the following.
