GitHub - akoprow/hybrid: Certified implementation of abstraction-based hybrid system safety prover.

Branches Tags

Name		Name	Last commit message	Last commit date
Latest commit History 139 Commits
ITP10		ITP10
doc		doc
examples		examples
haskell-impl		haskell-impl
old-nonconstructive		old-nonconstructive
web		web
.gitignore		.gitignore
Makefile		Makefile
README.html		README.html
SConstruct		SConstruct
TODO		TODO
TODO-history		TODO-history
Types.hs		Types.hs
abstract.v		abstract.v
abstract_as_graph.v		abstract_as_graph.v
abstract_cont_trans_over.v		abstract_cont_trans_over.v
bnat.v		bnat.v
bool_util.v		bool_util.v
bounded_rotator.v.bitrot		bounded_rotator.v.bitrot
c_util.v		c_util.v
clean.sh		clean.sh
concrete.v		concrete.v
containers.v		containers.v
coqdeps_as_dot.hs		coqdeps_as_dot.hs
decreasing_exponential_flow.v		decreasing_exponential_flow.v
digraph.v		digraph.v
flow.v		flow.v
geometry.v		geometry.v
graph_to_dot.hs		graph_to_dot.hs
hlist.v		hlist.v
hlist_aux.v		hlist_aux.v
hs_solver.v		hs_solver.v
hypercube_abstraction.v		hypercube_abstraction.v
hypergeometry.v		hypergeometry.v
interval_abstraction.v		interval_abstraction.v
interval_spec.v		interval_spec.v
list_util.v		list_util.v
monotonic_flow.v		monotonic_flow.v
nat_util.v		nat_util.v
square_abstraction.v		square_abstraction.v
square_flow_conditions.v		square_flow_conditions.v
stability.v		stability.v
tactics.v		tactics.v
util.v		util.v
vector_setoid.v		vector_setoid.v

Repository files navigation

<?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.2 (at the moment this precise version is required; newer versions will not work)</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>