JLiSA — Java Frontend of LiSA (Library for Static Analysis)

JLiSA is a static analysis tool for Java programs, built on top of the LiSA (Library for Static Analysis) framework. It provides a front-end that translates Java source files into LiSA's control flow graph (CFG) representation, enriches it with the semantics of a subset of the Java standard library, and runs configurable abstract interpretation analyses to detect bugs and verify program properties.

JLiSA is a joint effort between the Software and Systems Verification (SSV) Research Group at Ca' Foscari University of Venice and the University of Parma.

In its first participation at SV-COMP 2026 (15th International Competition on Software Verification), JLiSA achieved 3rd place in the Java track, earning the bronze medal. SV-COMP is the world's leading competition in automated software verification; results are presented at TACAS 2026, held in Turin, Italy, in April 2026.

Arceri et al., "JLiSA: The Java Frontend of the Library for Static Analysis" (Competition Contribution), SV-COMP 2026. Artifact: doi.org/10.5281/zenodo.17609338

Further details in the press releases from Ca' Foscari University and University of Parma.

• Overview
• Installation
• Usage
• Command-Line Options
• Architecture
• Development
• License

JLiSA translates Java source code into LiSA's intermediate representation and runs abstract interpretation analyses over the resulting program model. The analysis configuration is fully customizable — abstract domains, interprocedural strategy, and semantic checkers can all be selected independently. For SV-COMP 2026, JLiSA was configured with the following components:

• Field-sensitive, point-based heap abstraction — tracks heap objects at allocation sites with per-field sensitivity
• Reduced product of constant propagation and interval domain — abstracts numerical, string, and Boolean values
• Type inference — tracks runtime types of expressions
• Reachability analysis — distinguishes definitely reachable instructions from possibly reachable or unreachable ones, improving precision on conditional branches
• Call-string-based interprocedural analysis — context-sensitive up to 150 nested calls, with 0-CFA for call graph construction
• Semantic checkers — verifies assert statements and detects potential uncaught runtime exceptions

Prerequisites: Java 17+, Gradle (wrapper included), GitHub credentials for the LiSA dependency.

LiSA packages are hosted on GitHub Packages. Add your credentials to ~/.gradle/gradle.properties:

gpr.user=<your-github-username>
gpr.key=<your-github-personal-access-token>

Or export the environment variables USERNAME and TOKEN.

git clone https://github.com/lisa-analyzer/jlisa.git
cd jlisa/jlisa
./gradlew build

This runs code style checks and compiles the project. To produce a self-contained executable ZIP:

./gradlew distZip

The archive is written to build/distributions/jlisa-0.1.zip.

JLiSA has three sub-commands:

jlisa <sub-command> -h prints the options of a sub-command, and jlisa -v the version.

After building the distribution, run JLiSA directly:

./build/distributions/jlisa-0.1/bin/jlisa check -s path/to/File.java -o out/ -n ConstantPropagation

Or via Gradle without packaging:

./gradlew run --args="check -s path/to/File.java -o out/ -n ConstantPropagation"

Results are written to the output directory as a report.json summary. With --dump-graphs, the JSON graphs of the analysed methods (one per CFG) are written too, and with --dump-html, their HTML pages. With --svcomp-property, a violation witness is written for a definite violation of the property.

On an SV-COMP task (its input files and directories, and its property file):

jlisa check    -s common/ task/ -o out/ -n ConstantPropagation --svcomp-property valid-assert.prp
jlisa validate -s common/ task/ --svcomp-property valid-assert.prp -w witness.yml
jlisa find-bug -s common/ task/ --svcomp-property valid-assert.prp --witness-output witness.yml

validate and find-bug run the program under JDI: they need the modules jdk.compiler and jdk.jdi, which a JDK has (on Debian and Ubuntu, openjdk-N-jre-headless has them too). validate and find-bug print their verdict on a line of its own, after [VERDICT] (e.g. [VERDICT] Witness Correct).

--svcomp-property can be repeated: one witness for each property.

Java source code is parsed via the Eclipse Java Development Tools (JDT) library.

JLiSA's frontend translates Java source files to LiSA's IR in five sequential passes, implemented using the JDT visitor pattern in the following classes:

1. PopulateUnitsASTVisitor — registers all class and interface stubs in the program
2. SetRelationshipsASTVisitor — resolves superclass and interface relationships
3. SetGlobalsASTVisitor — registers fields and enum constants
4. InitCodeMembersASTVisitor — declares method and constructor signatures
5. CompilationUnitASTVisitor — performs full body translation, generating CFGs

Standard library classes are not parsed from source. Instead, hand-written stub files (src/main/resources/libraries/*.txt) declare class hierarchies, fields, and method signatures using a custom DSL parsed by an ANTLR grammar. Method semantics are implemented as Java classes under it.unive.jlisa.program.java.constructs. Stubs are loaded lazily at analysis time by LibrarySpecificationProvider.

# Run all tests
./gradlew test

# Run a single test class
./gradlew test --tests "it.unive.jlisa.cron.MathTest"

# Run a single test method
./gradlew test --tests "it.unive.jlisa.cron.MathTest.testMath"

Test inputs live in java-testcases/ and expected JSON outputs are stored alongside them. To regenerate expected outputs after an intentional change, temporarily set conf.forceUpdate = true in TestHelpers.

JLiSA uses Spotless (Eclipse formatter) and Checkstyle. Formatting uses tabs, not spaces.

# Check style
./gradlew checkCodeStyle

# Auto-fix formatting
./gradlew spotlessApply

This project is licensed under the MIT License.