JEvent is a static analysis and model generation framework for multithreaded Java programs. It implements an executable operational semantics of the Java Memory Model and generates event spaces that capture all possible executions of a concurrent Java program.
The project was developed during my PhD research on model checking concurrent Java software.
Traditional model checkers explore state spaces directly. JEvent instead represents the execution of a Java program as an event space, a partial-order structure describing memory operations, synchronization events, and thread interactions.
These event spaces can subsequently be: - reduced using slicing techniques, - transformed into finite-state automata, - model checked against temporal logic properties.
The objective is to make verification of concurrent Java programs more scalable by reducing the complexity of the explored state space while preserving correctness.
- Java parser and semantic model
- Executable operational semantics of the Java Memory Model
- Event-space generation for multithreaded Java programs
- Enumeration of nondeterministic thread schedules
- Partial-order representation of concurrent executions
- Event-space slicing
- Aliasing analysis
- Translation to finite-state automata
- Integration with PVS for CTL model checking
- OCaml
- Static Analysis
- Program Analysis
- Operational Semantics
- Model Checking
- Program Slicing
- Finite-State Automata
- PVS
This repository preserves the original research prototype developed during my PhD. It is no longer actively maintained.