Piklab is an integrated development environment for applications based on PIC and dsPIC microcontrollers. Supported compilers are: the Small Device C Compiler, the GNU PIC Utilities, PICC compilers, the PIC30 toolchain, the C18 compiler, the JAL and JALV2 compilers, the CSC compiler, and the Boost compilers. Supported programmers: ICD2, PICkit, PICkit2, PicStart+, and most direct programmers. Supported debuggers: ICD2 and GPSim. A commandline programmer/debugger is also provided.
BOUML is a UML 2 tool box that allows you to specify and generate code in C++, Java, IDL, and PHP. BOUML is very fast and doesn't require much memory to manage several thousands of classes. BOUML is extensible, and the external tools (named plug-outs) can be written in C++ or Java, using BOUML for their definition as any other program. UML models can be exported to HTML pages, including PNG or SVG graphics.
ACL2 is a mathematical logic, programming language, and mechanical theorem prover based on the applicative subset of Common Lisp. It is an "industrial-strength" version of the NQTHM or Boyer/Moore theorem prover, and has been used for the formal verification of commercial microprocessors, the Java Virtual Machine, interesting algorithms, and so forth.