Publications
- Andrius Velykis. Capturing Proof Process. PhD thesis, School of Computing Science, Newcastle University, UK, 2015.
@phdthesis{Velykis15, author = {Velykis, Andrius}, school = {School of Computing Science, Newcastle University, UK}, title = {Capturing Proof Process}, url = {http://andrius.velykis.lt/publications/Velykis15.pdf}, year = {2015} }Proof automation is a common bottleneck for industrial adoption of formal methods. Heuristic search techniques fail to discharge every proof obligation (PO), and significant effort is spent on proving the remaining ones interactively. Luckily, they usually fall into several proof families, where a single idea is required to discharge all similar POs. However, interactive formal proof requires expertise and is expensive: repeating the ideas over multiple proofs adds up to significant costs.
The AI4FM research project aims to alleviate the repetitive effort by “learning” from an expert doing interactive proof. The expert’s proof attempts can give rise to reusable strategies, which capture the ideas necessary to discharge similar POs. Automatic replay of these strategies would complete the remaining proof tasks within the same family, enabling the expert to focus on novel proof ideas.
This thesis presents an architecture to capture the expert’s proof ideas as a high-level proof process. Expert insight is not reflected in low-level proof scripts, therefore a generic ProofProcess framework is developed to capture high-level proof information, such as proof intent and important proof features of the proof steps taken. The framework accommodates branching to represent the actual proof structure as well as layers of abstraction to accommodate different granularities. The full history of how the proof was discovered is recorded, including multiple attempts to capture alternative, failed or unfinished versions.
A prototype implementation of the ProofProcess framework is available, including integrations with Isabelle and Z/EVES theorem provers. Two case studies illustrate how the ProofProcess systems are used to capture high-level proof processes in examples from industrial-style formal developments. Reuse of the captured information to discharge similar proofs within the examples is also explored.
The captured high-level information facilitates extraction of reusable proof strategies. Furthermore, the data could be used for proof maintenance, training, proof metrics, and other use cases.
- Leo Freitas, Cliff B. Jones, and Andrius Velykis. Can a system learn from interactive proofs? In Andrei Voronkov and Margarita Korovina, editors, HOWARD-60. A Festschrift on the Occasion of Howard Barringer’s 60th Birthday, pages 124–139. EasyChair, 2014.
@inproceedings{FreitasJV14, author = {Freitas, Leo and Jones, Cliff B. and Velykis, Andrius}, booktitle = {HOWARD-60. A Festschrift on the Occasion of {H}oward {B}arringer's 60th Birthday}, editor = {Voronkov, Andrei and Korovina, Margarita}, pages = {124--139}, publisher = {EasyChair}, title = {Can a system learn from interactive proofs?}, url = {http://andrius.velykis.lt/publications/FreitasJV14.pdf}, year = {2014} }This paper sets out the on-going research in a project which is investigating how to learn from one interactive proof so that other similar proofs can be completed automatically.
- Leo Freitas, Cliff B. Jones, Andrius Velykis, and Iain Whiteside. A Model for Capturing and Replaying Proof Strategies. In Dimitra Giannakopoulou and Daniel Kroening, editors, VSTTE 2014, volume 8471 of LNCS, pages 183–199. Springer, 2014. doi:10.1007/978-3-319-12154-3_12.
@inproceedings{FreitasJVW14, author = {Freitas, Leo and Jones, Cliff B. and Velykis, Andrius and Whiteside, Iain}, booktitle = {{VSTTE} 2014}, doi = {10.1007/978-3-319-12154-3_12}, editor = {Giannakopoulou, Dimitra and Kroening, Daniel}, isbn = {978-3-319-12153-6}, pages = {183--199}, publisher = {Springer}, series = {LNCS}, title = {A Model for Capturing and Replaying Proof Strategies}, volume = {8471}, url = {http://andrius.velykis.lt/publications/FreitasJVW14.pdf}, year = {2014} }Modern theorem provers can discharge a significant proportion of Proof Obligation (POs) that arise in the use of Formal Method (FMs). Unfortunately, the residual POs require tedious manual guidance. On the positive side, these “difficult” POs tend to fall into families each of which requires only a few key ideas to unlock. This paper outlines a system that can lessen the burden of FM proofs by identifying and characterising ways of discharging POs of a family by tracking an interactive proof of one member of the family. This opens the possibility of capturing ideas - represented as proof strategies - from an expert and/or maximising reuse of ideas after changes to definitions. The proposed system has to store a wealth of meta-information about conjectures, which can be matched against previously learned strategies, or can be used to construct new strategies based on expert guidance.
- Cliff B. Jones, Leo Freitas, and Andrius Velykis. Ours Is to Reason Why. In Zhiming Liu, Jim Woodcock, and Huibiao Zhu, editors, Theories of Programming and Formal Methods - Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday, volume 8051 of Lecture Notes in Computer Science, pages 227–243, Shanghai, China, September 2013. Springer. doi:10.1007/978-3-642-39698-4_14.
@inproceedings{JonesFV13, address = {Shanghai, China}, author = {Jones, Cliff B. and Freitas, Leo and Velykis, Andrius}, booktitle = {Theories of Programming and Formal Methods - Essays Dedicated to {J}ifeng {H}e on the Occasion of His 70th Birthday}, doi = {10.1007/978-3-642-39698-4_14}, editor = {Liu, Zhiming and Woodcock, Jim and Zhu, Huibiao}, month = sep, pages = {227--243}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {Ours Is to Reason Why}, url = {http://andrius.velykis.lt/publications/JonesFV13.pdf}, volume = {8051}, year = {2013} }It is now widely understood how to write formal specifications so as to be able to justify designs (and thus implementations) against such specifications. In many formal approaches, a “posit and prove” approach allows a designer to record an engineering design decision from which a collection of “proof obligations” are generated; their discharge justifies the design step. Modern theorem proving tools greatly simplify the discharge of such proof obligations. In typical industrial applications, however, there remain sufficiently many proof obligations that require manual intervention that an engineer finds them a hurdle to the deployment of formal proofs. This problem is exacerbated by the need to repeat proofs when changes are made to specifications or designs. This paper outlines how a key additional resource can be brought to bear on the discharge of proof obligations: the central idea is to “learn” new ways of discharging families of proof obligations by tracking one interactive proof performed by an expert. Since what blocks any fixed set of heuristics from automatically discharging proof obligations is issues around data structures and/or functions, it is expected that what the system can learn from one interactive proof will facilitate the discharge of significant “families” of recalcitrant proof tasks.
- Leo Freitas, Cliff B. Jones, Andrius Velykis, and Iain Whiteside. How to say why (in AI4FM). Technical Report CS-TR-1398, School of Computing Science, Newcastle University, October 2013.
@techreport{FreitasJVW13, author = {Freitas, Leo and Jones, Cliff B. and Velykis, Andrius and Whiteside, Iain}, institution = {School of Computing Science, Newcastle University}, month = oct, number = {CS-TR-1398}, title = {How to say why (in {AI4FM})}, url = {http://www.cs.ncl.ac.uk/publications/trs/papers/1398.pdf}, year = {2013} }In the AI4FM project we have set ourselves the challenge of building a system that can learn high-level proof strategies by monitoring expert users. A typical level of ambition is users who are proving the feasibility and reification of medium-sized specifications. The purpose of this report is to provide a source document. In particular, it (a) summarises some experiments in the use of verification tools to determine how realistic the ambition is of extracting the “why” from experts’ use of verification tools; and, (b) provides a revision of an earlier description of an abstract model of an AI4FM system that is linked to the case studies.
- Andrius Velykis. Inferring the Proof Process. In Christine Choppy, David Delayahe, and Kaïs Klaï, editors, FM2012 Doctoral Symposium, Paris, France, August 2012.
@inproceedings{Velykis12, address = {Paris, France}, author = {Velykis, Andrius}, booktitle = {FM2012 Doctoral Symposium}, editor = {Choppy, Christine and Delayahe, David and Kla\"{i}, Ka\"{i}s}, month = aug, title = {Inferring the Proof Process}, url = {http://andrius.velykis.lt/publications/Velykis12.pdf}, year = {2012} }This PhD project aims to investigate how enough information can be collected from an interactive formal proof to capture an expert’s ideas as a high-level proof process. It would then serve for extracting proof strategies to facilitate proof automation. Ways of inferring this proof process automatically are explored; and a family of tools is developed to capture the different proof processes and their features.
- Andrius Velykis. Capturing and Inferring the Proof Process (Part 2: Architecture). In Alan Bundy, Dieter Hutter, Cliff B. Jones, and J Strother Moore, editors, AI meets Formal Software Development, number 12271 in Dagstuhl Seminar Proceedings, pages 27–27, Dagstuhl, Germany, 2012. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany. doi:10.4230/DagRep.2.7.1.
@inproceedings{Velykis12a, address = {Dagstuhl, Germany}, author = {Velykis, Andrius}, booktitle = {AI meets Formal Software Development}, doi = {10.4230/DagRep.2.7.1}, editor = {Bundy, Alan and Hutter, Dieter and Jones, Cliff B. and Moore, J Strother}, number = {12271}, pages = {27--27}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany}, series = {Dagstuhl Seminar Proceedings}, title = {Capturing and Inferring the Proof Process ({P}art 2: Architecture)}, url = {http://drops.dagstuhl.de/opus/volltexte/2012/3731/pdf/dagrep_v002_i007_p001_s12271.pdf}, year = {2012} } - Andrius Velykis and Leo Freitas. Formal Modelling of Separation Kernel Components. In Ana Cavalcanti, David Déharbe, Marie-Claude Gaudel, and Jim Woodcock, editors, ICTAC 2010, volume 6255 of Lecture Notes in Computer Science, pages 230–244. Springer, 2010. doi:10.1007/978-3-642-14808-8_16.
@inproceedings{VelykisF10, author = {Velykis, Andrius and Freitas, Leo}, booktitle = {ICTAC 2010}, doi = {10.1007/978-3-642-14808-8_16}, editor = {Cavalcanti, Ana and D{\'e}harbe, David and Gaudel, Marie-Claude and Woodcock, Jim}, pages = {230--244}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {Formal Modelling of Separation Kernel Components}, url = {http://andrius.velykis.lt/publications/VelykisF10.pdf}, volume = {6255}, year = {2010} }Separation kernels are key components in embedded applications. Their small size and widespread use in high-integrity environments make them good targets for formal modelling and verification. We summarise results from the mechanisation of a separation kernel scheduler using the Z/Eves theorem prover. We concentrate on key data structures to model scheduler operations. The results are part of an experiment in a Grand Challenge in software verification, as part of a pilot project in verified OS kernels. The project aims at creating a mechanised formal model of kernel components that gets refined to code. This provides a set of reusable components, proof strategies, and general lemmas. Important findings about properties and requirements are also discussed.
- Andrius Velykis. Formal Modelling of Separation Kernels. Master’s thesis, Department of Computer Science, University of York, UK, September 2009.
@mastersthesis{Velykis09, author = {Velykis, Andrius}, month = sep, school = {Department of Computer Science, University of York, UK}, title = {Formal Modelling of Separation Kernels}, url = {http://andrius.velykis.lt/publications/Velykis09.pdf}, year = {2009} }A separation kernel is an architecture for secure applications, which benefits from inherent security of distributed systems. Due to its small size and usage in high-integrity environments, it makes a good target for formal modelling and verification. This project presents results from mechanisation and modelling of separation kernel components: a process table, a process queue and a scheduler. The results have been developed as a part of the pilot project within the international Grand Challenge in Verified Software. This thesis covers full development life-cycle from project initiation through design and evaluation to successful completion. Important findings about kernel properties, formal modelling and design decisions are discussed. The developed formal specification is fully verified and contributes to the pilot project aim of creating a formal kernel model and refining it down to implementation code. Other reusable artefacts, such as general lemmas and a new technique of ensuring transactional properties of operations are defined. The results will be curated within the Verified Software Repository.