Certified implementation of abstraction-based hybrid system safety prover.
Coq Haskell Other
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
ITP10 final ? updates Apr 8, 2010
doc doc: Fix university name and credit BRICKS/FOCUS project. Feb 1, 2010
examples Make examples/thermostat/safe compile with current Coq/CoRN/CoLoR. Nov 3, 2012
haskell-impl Add nice and simple Haskell implementation showing the "hacks". Aug 26, 2009
old-nonconstructive Move old non-constructive development into subdir, and get rid of c_ … Apr 23, 2009
web Add web page. Jan 22, 2010
.gitignore .gitignore *.glob. Jun 17, 2010
Makefile Room heating put in separate directory; added CoLoR library to SConst… Jun 10, 2009
README.html Update to Coq 8.2pl1. Jun 4, 2010
SConstruct Make examples/thermostat/safe compile with current Coq/CoRN/CoLoR. Nov 3, 2012
TODO Lots and lots of improvements, restructuring, clarification, cleanup. Sep 15, 2009
TODO-history Set-up for extraction; some boilerplate code in thermostat replaced w… May 17, 2009
abstract.v Make examples/thermostat/safe compile with current Coq/CoRN/CoLoR. Nov 3, 2012
abstract_as_graph.v Make examples/thermostat/safe compile with current Coq/CoRN/CoLoR. Nov 3, 2012
abstract_cont_trans_over.v Make examples/thermostat/safe compile with current Coq/CoRN/CoLoR. Nov 3, 2012
bnat.v Make examples/thermostat/safe compile with current Coq/CoRN/CoLoR. Nov 3, 2012
bool_util.v Removing vec_util and instead using CoLoR (to avoid duplication and m… Jun 6, 2009
bounded_rotator.v.bitrot Revive unbounded_rotator. Move it and thermostat to examples subdir. … Jun 5, 2009
c_util.v Make examples/thermostat/safe compile with current Coq/CoRN/CoLoR. Nov 3, 2012
clean.sh Make thermostat more closely resemble Alur's. Use Program to make som… Apr 23, 2009
concrete.v Make examples/thermostat/safe compile with current Coq/CoRN/CoLoR. Nov 3, 2012
containers.v Make examples/thermostat/safe compile with current Coq/CoRN/CoLoR. Nov 3, 2012
coqdeps_as_dot.hs Update dependency visualization script. Specialize it for thermostat. Jun 12, 2009
decreasing_exponential_flow.v Make examples/thermostat/safe compile with current Coq/CoRN/CoLoR. Nov 3, 2012
digraph.v Make examples/thermostat/safe compile with current Coq/CoRN/CoLoR. Nov 3, 2012
flow.v Make examples/thermostat/safe compile with current Coq/CoRN/CoLoR. Nov 3, 2012
geometry.v Make examples/thermostat/safe compile with current Coq/CoRN/CoLoR. Nov 3, 2012
hlist.v Switching to hlist_aux in abstract to define n-dimensional space; alm… Apr 13, 2010
hlist_aux.v Make examples/thermostat/safe compile with current Coq/CoRN/CoLoR. Nov 3, 2012
hs_solver.v Lots and lots of improvements, restructuring, clarification, cleanup. Sep 15, 2009
hypercube_abstraction.v Transcribing the content of [square_abstraction.v] to [hypercube_abst… Apr 13, 2010
hypergeometry.v Transcribing the content of [square_abstraction.v] to [hypercube_abst… Apr 13, 2010
interval_abstraction.v Make examples/thermostat/safe compile with current Coq/CoRN/CoLoR. Nov 3, 2012
interval_spec.v Make examples/thermostat/safe compile with current Coq/CoRN/CoLoR. Nov 3, 2012
list_util.v Make examples/thermostat/safe compile with current Coq/CoRN/CoLoR. Nov 3, 2012
monotonic_flow.v Make examples/thermostat/safe compile with current Coq/CoRN/CoLoR. Nov 3, 2012
nat_util.v Proven invariant stability for the room heating. May 18, 2010
square_abstraction.v Make examples/thermostat/safe compile with current Coq/CoRN/CoLoR. Nov 3, 2012
square_flow_conditions.v Make examples/thermostat/safe compile with current Coq/CoRN/CoLoR. Nov 3, 2012
stability.v Make examples/thermostat/safe compile with current Coq/CoRN/CoLoR. Nov 3, 2012
tactics.v hyper_space (2D space generalized to n dimensions) defined except for… Apr 13, 2010
util.v Make examples/thermostat/safe compile with current Coq/CoRN/CoLoR. Nov 3, 2012
vector_setoid.v Make examples/thermostat/safe compile with current Coq/CoRN/CoLoR. Nov 3, 2012

README.html

<?xml version='1.0' encoding='UTF-8'?>

<!DOCTYPE html PUBLIC '-//W3C//DTD XHTML 1.1//EN' 'http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd'>
<html xmlns='http://www.w3.org/1999/xhtml' xml:lang='en'>
  <head>
    <title>Readme</title>
  </head>
  <body>
    <h1>Readme</h1>

    <hr/><h2>1. Prerequisites</h2>

    <ul>
      <li><a href='http://coq.inria.fr/'>Coq</a> 8.2pl1</li>
      <li><a href='http://coq.inria.fr/distrib/current/contribs/CoRN.html'>CoRN</a></li>
      <li><a href='http://color.inria.fr/download-color.html'>CoLoR</a></li>
      <li><a href='http://www.scons.org/'>SCons</a> &ge; 0.98 (SCons is a modern make-replacement based on Python)</li>
    </ul>

    <hr/><h2>2. Compilation</h2>

    <p>Simply invoking "<kbd>scons</kbd>" in the current directory should compile the entire development.</p>
  </body>
</html>