Sciweavers

LICS
2012
IEEE
11 years 6 months ago
Logics of Dynamical Systems
—We study the logic of dynamical systems, that is, logics and proof principles for properties of dynamical systems. Dynamical systems are mathematical models describing how the s...
André Platzer
IANDC
2006
93views more  IANDC 2006»
13 years 4 months ago
Automation for interactive proof: First prototype
Interactive theorem provers require too much effort from their users. We have been developing a system in which Isabelle users obtain automatic support from automatic theorem prov...
Jia Meng, Claire Quigley, Lawrence C. Paulson
MKM
2009
Springer
13 years 10 months ago
Combining Coq and Gappa for Certifying Floating-Point Programs
Abstract. Formal verification of numerical programs is notoriously difficult. On the one hand, there exist automatic tools specialized in floatingpoint arithmetic, such as Gappa...
Sylvie Boldo, Jean-Christophe Filliâtre, Gui...
CADE
2004
Springer
14 years 4 months ago
Experiments on Supporting Interactive Proof Using Resolution
Interactive theorem provers can model complex systems, but require much effort to prove theorems. Resolution theorem provers are automatic and powerful, but they are designed to be...
Jia Meng, Lawrence C. Paulson