tomahawkins/acl2

Stars
2
Language
Haskell
License
Other
Created about 10 years ago
Updated about 10 years ago

tomahawkins/acl2

tomahawkins

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

Writing and calling ACL2 from Haskell.

atom

A DSL for embedded hard realtime applications.

improve

An imperative programming language in Haskell for high assurance embedded applications. ImProve programs are verified with model checking. ImProve compiles to C and Simulink.

ecu

Utilities for automotive ECU development.

verilog

A Verilog parser for Haskell.

mecha

A solid modeling language in Haskell.

ccnx

A Haskell platform for experimenting with content centric networking.

afv

C model checking.

smt-lib

Parsing and printing SMT-LIB from Haskell.

binding-templates

Alpine binding mounting templates.

powerpc

Tools for PowerPC programs.

vcd

A small library for generating VCD files.

asm-dsl-example

An example showing how to build an assembly DSL in Haskell.

fountain

A fountain codec in Haskell.

powerpc-eabi

Scripts and patches to build a GCC cross compiler (C, C++, Ada) for bare metal PowerPC targets.

engineering-units

A numeric type to automatically manage engineering units in Haskell.

theoremquest

ltl

Tools for testing embedded software with linear temporal logic.

ivory-backend-acl2

An Ivory to ACL2 compiler.

risk

A Realtime Information-flow-control Separation Kernel

srec

Reading S-Record files from Haskell.

fault-tree

A fault tree analysis library.

cil

A Haskell interface to CIL.

lmor

sudoku

A simple sudoku solver in Haskell.

trs

Hardware description language based on conditional term rewriting systems.

volleyball

hydraulics

A gschem symbol library for describing hydraulic circuits.

statechart

Compiles Rhapsody statecharts to C.

verilog-gt

devsurf

A DSL for creating developable surfaces.

fp-intro

Introduction to Functional Programming

hydro

A design of a hydroplane using devsurf.

clutch-control-example

A ImProve example for control systems.

atom-hd

An Atom DSL for hardware design.

dove

blocking

emsec

hitting

rtl

A simple logic design DSL.

ni-proofs

Proofs of noninterference IFC security properties.

sls

Switch level synthesis using SMT.

monopoly

heavylift

outboard

Outboard maintenance course.

fcnav

A map to help navigate your way through the Fort Custer Maze in Clear Lake, IA.

circ

A compiler IR compiler.

track

Computed diagrams of possible slot car track layouts.

bmp

trackcad

A CAD library for designing tracked vehicles.

gigl

A simple imperative language.