Publications

From BWare
Jump to: navigation, search

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. (PDF)
  • 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. (PDF)
  • 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. (PDF)
  • 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. (PDF)
  • 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. (PDF)
  • 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. (PDF)
  • 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. (PDF)

National Conferences

  • David Delahaye, Claude Marché, and David Mentré. Le projet BWare : une plate-forme pour la vérification automatique d'obligations de preuve B. In Catherine Dubois and Régine Laleau, editors, Approches Formelles dans l’Assistance au Développement de Logiciels (AFADL), Paris (France), June 2014. To appear. (PDF)
Personal tools
Namespaces

Variants
Actions
Navigation
Toolbox