# Publications

From BWare

(Difference between revisions)

(→International Conferences) |
(→International Conferences) |
||

Line 7: | Line 7: | ||

* David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand, and Olivier Hermant. Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo. In Ken McMillan, Aart Middeldorp, and Voronkov Andrei, editors, ''Logic for Programming Artificial Intelligence and Reasoning (LPAR)'', volume 8312 of ''Lecture Notes in Computer Science (LNCS)/Advanced Research in Computing and Software Science (ARCoSS)'', pages 274—290, Stellenbosch (South Africa), December 2013. Springer. | * David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand, and Olivier Hermant. Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo. In Ken McMillan, Aart Middeldorp, and Voronkov Andrei, editors, ''Logic for Programming Artificial Intelligence and Reasoning (LPAR)'', volume 8312 of ''Lecture Notes in Computer Science (LNCS)/Advanced Research in Computing and Software Science (ARCoSS)'', pages 274—290, Stellenbosch (South Africa), December 2013. Springer. | ||

* David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand, and Olivier Hermant. Proof Certification in Zenon Modulo: When Achilles Uses Deduction Modulo to Outrun the Tortoise with Shorter Steps. In Ken McMillan, Aart Middeldorp, and Voronkov Andrei, editors, ''International Workshop on the Implementation of Logics (IWIL)'', Stellenbosch (South Africa), December 2013. EasyChair. To appear. | * David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand, and Olivier Hermant. Proof Certification in Zenon Modulo: When Achilles Uses Deduction Modulo to Outrun the Tortoise with Shorter Steps. In Ken McMillan, Aart Middeldorp, and Voronkov Andrei, editors, ''International Workshop on the Implementation of Logics (IWIL)'', Stellenbosch (South Africa), December 2013. EasyChair. To appear. | ||

− | * Guillaume Burel. A Shallow Embedding of Resolution and Superposition Proofs into the λ | + | * Guillaume Burel. A Shallow Embedding of Resolution and Superposition Proofs into the λΠ-Calculus Modulo. In ''Proof Exchange for Theorem Proving (PxTP)'', volume 14 of ''EPiC''. EasyChair, 2013. |

== National Conferences == | == National Conferences == |

## Revision as of 15:00, 27 September 2014

## International Conferences

- Jean-Christophe Filliâtre, Léon Gondelman, and Andrei Paskevich. The Spirit of Ghost Code. In Armin Biere and Roderick Bloem, editors,
*Computer Aided Verification (CAV)*, volume 8559 of*Lecture Notes in Computer Science (LNCS)*, pages 1—16, Vienna (Austria), July 2014. Springer. - Martin Clochard, Jean-Christophe Filliâtre, Claude Marché, and Andrei Paskevich. Formalizing Semantics with an Automatic Program Verifier. In Dimitra Giannakopoulou and Daniel Kroening, editors,
*Verified Software: Theories, Tools and Experiments (VSTTE)*, volume 8471 of*Lecture Notes in Computer Science (LNCS)*, Vienna (Austria), July 2014. Springer. - David Delahaye, Catherine Dubois, Claude Marché, and David Mentré. The BWare Project: Building a Proof Platform for the Automated Verification of B Proof Obligations. In Yamine Ait Ameur and Klaus-Dieter Schewe, editors,
*Abstract State Machines, Alloy, B, VDM, and Z (ABZ)*, Lecture Notes in Computer Science (LNCS), Toulouse (France), June 2014. Springer. To appear. - Sylvain Conchon and Mohamed Iguernelala . Tuning the Alt-Ergo SMT Solver for B Proof Obligations. In Yamine Ait Ameur and Klaus-Dieter Schewe, editors,
*Abstract State Machines, Alloy, B, VDM, and Z (ABZ)*, Lecture Notes in Computer Science (LNCS), Toulouse (France), June 2014. Springer. To appear. - David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand, and Olivier Hermant. Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo. In Ken McMillan, Aart Middeldorp, and Voronkov Andrei, editors,
*Logic for Programming Artificial Intelligence and Reasoning (LPAR)*, volume 8312 of*Lecture Notes in Computer Science (LNCS)/Advanced Research in Computing and Software Science (ARCoSS)*, pages 274—290, Stellenbosch (South Africa), December 2013. Springer. - David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand, and Olivier Hermant. Proof Certification in Zenon Modulo: When Achilles Uses Deduction Modulo to Outrun the Tortoise with Shorter Steps. In Ken McMillan, Aart Middeldorp, and Voronkov Andrei, editors,
*International Workshop on the Implementation of Logics (IWIL)*, Stellenbosch (South Africa), December 2013. EasyChair. To appear. - Guillaume Burel. A Shallow Embedding of Resolution and Superposition Proofs into the λΠ-Calculus Modulo. In
*Proof Exchange for Theorem Proving (PxTP)*, volume 14 of*EPiC*. EasyChair, 2013.