2012/11/06 by Thai Son Hoang, Hoang, Thai Son
Computer Science · #Distributed systems and fault tolerance #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Software Engineering (cs.SE) #Software Testing and Debugging Techniques
paper · pdf · doi:10.48550/arxiv.1211.1172
openalex publication_date 2012/11/06 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Interactive proofs are often considered as costs of formal modelling activity. In an incremental development environment such as the Rodin platform for Event-B, information from proof attempts is important input for adapting the model. This paper considers the idea of using interactive proofs to "improve" the model, in particular, to convert them into automatic ones. We propose to lift some essential proof information from the interactive proofs into the model as what we called proof hints. In particular, proof hints are not only for the purpose of proofs: it helps to understand the formal models better.