Group: Key Project

Sort by:Popular▼

✓Popular✓Newest

Core functionality (terms, rules, prover, ...) for deductive verification of Java programs

Key Project Proofjava

User interface for the deductive verification of Java programs

Utility library of the key-project

Generic data strutures for terms and formulas without dependencies to a specific target programming language

Key Project Ips4o

Pattern Matchern New core KeY theorem prover

Proof slicing (removing of unnecessary nodes) for the KeY system.

Information-Flow / Non-interference calculus for Java using the KeY theorem prover

Test Case Generation based on proof attempts.

Well-defined calculus for JML specifciation and Java using the KeY theorem prover

Compiling Matching Algorithm of the KeY theorem prover

Caching of provable nodes to make proving with KeY faster.

Proof exploration capabilities for key.ui

Translation of Sequents to Isabelle

Management of larger verification with KeY.

Extension for key.ui to access the Test Case Generation graphically

API for using KeY as a symbolic execution engine for Java programs

API for using KeY for maintaining references between objects in proofs

Support for the RS3 Information Flow Language (RIFL)