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.

---

🥉 SV-COMP 2026 — Bronze Medal

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.

The Team

| Name | Institution | |---|---| | Vincenzo Arceri | University of Parma | | Luca Negrini | Ca' Foscari University of Venice | | Giacomo Zanatta | Ca' Foscari University of Venice | | Filippo Bianchi | University of Parma | | Teodors Lisovenko | Ca' Foscari University of Venice | | Luca Olivieri | Ca' Foscari University of Venice | | Pietro Ferrara | Ca' Foscari University of Venice |

---

Table of Contents

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

---

Overview

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

---

Installation

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

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.

Build

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.

---

Usage

After building the distribution, run JLiSA directly:

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

Or via Gradle without packaging:

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

Results are written to the output directory as JSON files (one per CFG) and a report.json summary.

---

Command-Line Options

| Option | Long Option | Argument | Description | |--------|-------------|----------|-------------| | -s | --source | file... | Java source files to analyze (space-separated) | | -o | --outdir | path | Output directory for analysis results | | -n | --numericalDomain | domain | Numerical domain: ConstantPropagation | | -c | --checker | checker | Semantic checker: Assert | | -l | --log-level | level | Log verbosity: INFO, DEBUG, WARN, ERROR, OFF | | -m | --mode | mode | Execution mode: Debug (default), Statistics | | -v | --version | — | Print the tool version | | -h | --help | — | Print the help message | | N/A | --no-html | — | Disable HTML output (enabled by default) |

---

Architecture

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

Java Standard Library

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.

Key Packages

| Package | Purpose | |---|---| | it.unive.jlisa.frontend | Parsing pipeline, JavaFrontend, ParserContext | | it.unive.jlisa.frontend.util | Shared utilities (e.g. FQNUtils for building fully qualified names) | | it.unive.jlisa.frontend.visitors | AST visitor base classes and hierarchy | | it.unive.jlisa.program.cfg.expression | Java-specific expression nodes | | it.unive.jlisa.program.cfg.statement | Java-specific statement nodes | | it.unive.jlisa.program.java.constructs | Library method semantics | | it.unive.jlisa.program.libraries | Library stub loader | | it.unive.jlisa.program.type | Java type system | | it.unive.jlisa.analysis | Abstract domains (heap, value, type) | | it.unive.jlisa.interprocedural | Call graph and interprocedural analysis | | it.unive.jlisa.checkers | Semantic checkers (AssertChecker) | | it.unive.jlisa.witness | Violation witness generation (GraphML) |

---

Development

Running Tests

# 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.

Code Style

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

# Check style
./gradlew checkCodeStyle

# Auto-fix formatting
./gradlew spotlessApply

---

License

This project is licensed under the MIT License.