improve alternatives and similar packages
Based on the "Embedded" category.
Alternatively, view improve alternatives based on common mentions on social networks and blogs.
-
copilot
A (Haskell DSL) stream language for generating hard real-time C code. -
-
copilot-language
A Haskell-embedded DSL for monitoring hard real-time distributed systems. -
atom-msp430
Definitions for using Atom with the MSP430 microcontroller family. -
copilot-core
Intermediate representation for CoPilot. Strictly follows Haskell 2010 except for universal and existential quantification. -
copilot-libraries
Copilot libraries that use the Copilot language
Access the most powerful time series database as a service
Do you think we are missing an alternative of improve or a related project?
|
Clean code begins in your IDE with SonarLint
sponsored
www.sonarlint.org
|
Popular Comparisons
|
SaaSHub - Software Alternatives and Reviews
sponsored
www.saashub.com
|
README
ImProve
ImProve is an imperative programming language embedded in Haskell for high assurance applications. ImProve uses infinite state, unbounded model checking to verify programs adhere to specifications. Yices (required) is the backend SMT solver.
ImProve compiles to C, Ada, Simulink, and Modelica for implementation and system simulation.
Links
Release Notes
0.4.1 ???
0.4.0 07/29/11
- Automatic lemma inclusion. Changed 'theorem' to 'assert'. Removed 'Theorem' type.
0.3.4 04/18/11
- Ada code generation.
- Exported var and zero.
0.3.3 04/07/11
- Modelica model generation.
- 'assume' returns 'Theorem' types to act as lemmas to other theorems. Assumptions are not longer applied program wide.
- Added #ifdef __cplusplus to generated C header.
- Fixed conditionals for assertions in Simulink generation.
0.3.2 04/02/11
- Apply lemmas in all inductive steps except the last (instead of just at the begining).
- Removed hidden step 1.
0.3.1 03/28/11
- Simulink remove null effect optimization.
- Haddock documentation.
0.3.0 03/28/11
- Simulink model generation.
- Removed UV types.
0.2.3 12/13/10
- Fixed haddock documentation.
0.2.2 12/12/10
- Theorem name formatting (removed unique identifer).
- Better trace formatting.
0.2.1 12/09/10
- bugfix: lemmas referenced in induction step.
0.2.0 12/08/10
- Released 'assert' with 'theorem', which provides control of k and the ability to provide lemmas to simplify the proof.
- Verification assumes property is true for inductive steps up to k. Reduces the number of steps to converge on proof for some invariants.
0.1.6 12/02/10
- Made Statement an instance of Show.
- Made V a an instance of Eq and Ord.
- Created untyped variables (UV) and extended varInfo.
- Bugfix: shadow variable in Label collides with structure name.
0.1.5 11/23/10
- Loosened mtl requirements (mtl < 2.1).
0.1.4 11/22/10
- Bugfix: verification programming trimming: expressions in assertions in if statements not captured.
- Better annotation for assertions.
0.1.3 11/18/10
- Started state space narrowing optimizations: simple code analysis that reduce narrow the reachable state, thus reducing the number of inconclusive results.