AI4FM: using AI to aid automation of proof search in Formal Methods
Lead Research Organisation:
University of Edinburgh
Department Name: Sch of Informatics
Abstract
Abstracts are not currently available in GtR for all funded research. This is normally because the abstract was not required at the time of proposal submission, but may be because it included sensitive information such as personal details.
Organisations
Publications
Maclean E
(2016)
Proof automation for functional correctness in separation logic
in Journal of Logic and Computation
Lin Y
(2019)
Automating Event-B invariant proofs by rippling and proof patching
in Formal Aspects of Computing
Lin Y
(2012)
NASA Formal Methods
Jones, CB
(2010)
Ideas for a high-level proof strategy language
in 5th Automated Formal Methods workshop (AFM'10)
Grov, G
(2010)
A small experiment in Event-B rippling
in Proceedings of AVoCS 2010 and Rodin User and Developer Workshop 2010
Grov G
(2014)
Tinker, tailor, solver, proof
in Electronic Proceedings in Theoretical Computer Science
Grov G
(2017)
The Tinker tool for graphical tactic development
in International Journal on Software Tools for Technology Transfer
Freitas L
(2013)
Formalizing workflows partitioning over federated clouds: multi-level security and costs
in International Journal of Computer Mathematics
Description | Please see the details on the grant EP/H024050/1 - this is the grant owned by the lead site at Newcastle. |
Exploitation Route | Please see the details on the grant EP/H024050/1 - this is the grant owned by the lead site at Newcastle. |
Sectors | Other |
Description | Please see the details on the grant EP/H024050/1 - this is the grant owned by the lead site at Newcastle. |