Items where Subject is "Tool developments > Provers"

Voisin, Laurent (2013) Mathematical Language of Event-B Proofs. [Rodin Archive]

Déharbe, David and Fontaine, Pascal and Guyot, Yoann and Voisin, Laurent (2012) SMT Solvers for Rodin. In: ABZ 2012, 19-21 June 2012, Pisa, Italy.

Iliasov, Alexei (2011) Generation of certifiably correct programs from formal models. In: 1st Int. Workshop on Software Certification. At the 22nd Int. Symposium on Software Reliability Engineering (ISSRE 2011). , November 30, 2011, Hiroshima, Japan.

Maamria, Issam and Butler, Michael (2010) Rewriting and Well-Definedness within a Proof System. In: Partiality and Recursion in Interactive Theorem Provers PAR-10.

Butler, Michael and Maamria, Issam (2010) Mathematical Extension in Event-B through the Rodin Theory Component. Technical Report. Deploy Project. (Unpublished)

Maamria, Issam and Butler, Michael and Edmunds, Andrew and Rezazadeh, Abdolbaghi (2010) On an Extensible Rule-based Prover for Event-B. In: ABZ2010. (In Press)

Bundy, Alan and Grov, Gudmund and Jones, Cliff B (2009) An outline of a proposed system that learns from experts how to discharge proof obligations automatically. In: Dagstuhl seminar on Refinement Based Methods for the Construction of Dependable Systems, 14-18 Sept. 2009, Schloss Dagstuhl. (In Press)

Bundy, Alan and Grov, Gudmund and Jones, Cliff B (2009) Learning from experts to aid the automation of proof search. In: 9th International Workshop on Automated Verification of Critical Systems: AVoCS 2009. (In Press)

Fitzgerald, John S and Jones, Cliff B (2008) The connection between two ways of reasoning about partial functions. Information Processing Letters, 107 (3-4). pp. 128-132.

Bendisposto, Jens and Leuschel, Michael and Ligot, Olivier and Samia, Mireille (2008) La validation de modèles Event-B avec le plug-in ProB pour RODIN. TSI . pp. 1065-1084.

Jones, Cliff B (2008) Reflections on, and predictions for, support systems for the development of programs. In: ASE-08.

Wright, Stephen A Formally Constructed Instruction Set Architecture Definition of the XCore Microprocessor. [DEPLOY Associate Item]

Konrad, Matthias and Voisin, Laurent Translation from Set-Theory to Predicate Calculus. Technical Report. ETH Zurich. (Unpublished)