improve alternatives and similar packages
Based on the "Embedded" category.
Alternatively, view improve alternatives based on common mentions on social networks and blogs.
atom9.6 0.0 improve VS atomA DSL for embedded hard realtime applications.
copilot9.4 0.0 improve VS copilotA (Haskell DSL) stream language for generating hard real-time C code.
ecu8.6 0.0 improve VS ecuUtilities for automotive ECU development.
verilog8.2 0.0 improve VS verilogA Verilog parser for Haskell.
ion7.2 0.0 improve VS ionAn Ivory library inspired by Atom
copilot-language6.6 0.0 improve VS copilot-languageA Haskell-embedded DSL for monitoring hard real-time distributed systems.
atom-msp4306.1 0.0 improve VS atom-msp430Definitions for using Atom with the MSP430 microcontroller family.
copilot-sbv5.8 0.0 improve VS copilot-sbvSBV backend for Copilot.
fault-tree4.0 0.0 improve VS fault-treeA fault tree analysis library.
copilot-core4.0 0.0 improve VS copilot-coreIntermediate representation for CoPilot. Strictly follows Haskell 2010 except for universal and existential quantification.
copilot-libraries3.8 0.0 improve VS copilot-librariesCopilot libraries that use the Copilot language
copilot-cbmc3.2 0.0 improve VS copilot-cbmccbmc based tool for verifying copilot programs
copilot-c992.6 0.0 improve VS copilot-c99A C99-backend for Copilot
Access the most powerful time series database as a service
Do you think we are missing an alternative of improve or a related project?
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.
- Automatic lemma inclusion. Changed 'theorem' to 'assert'. Removed 'Theorem' type.
- Ada code generation.
- Exported var and zero.
- 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.
- Apply lemmas in all inductive steps except the last (instead of just at the begining).
- Removed hidden step 1.
- Simulink remove null effect optimization.
- Haddock documentation.
- Simulink model generation.
- Removed UV types.
- Fixed haddock documentation.
- Theorem name formatting (removed unique identifer).
- Better trace formatting.
- bugfix: lemmas referenced in induction step.
- 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.
- 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.
- Loosened mtl requirements (mtl < 2.1).
- Bugfix: verification programming trimming: expressions in assertions in if statements not captured.
- Better annotation for assertions.
- Started state space narrowing optimizations: simple code analysis that reduce narrow the reachable state, thus reducing the number of inconclusive results.