LiquidJava
Catch bugs before runtime with compile-time verification
LiquidJava adds refinement types and typestates to Java through annotations, enabling static verification that catches errors traditional type systems miss.
@Refinement("a > 0")
int a = 3; // ✓ verified safe
a = -8; // ✗ compile error- Refinement types - Express constraints beyond basic types
- Typestate verification - Track object state transitions
- SMT-backed - Powered by Z3 solver
- IDE integration - Real-time feedback in VS Code
- Lightweight - Annotation-based, works with existing Java code
📦 VS Code Extension
📚 Tutorial
💡 Examples
📖 Research Paper (ICSE 2023)
Learn more in the LiquidJava website.
Pinned Loading
Repositories
- vscode-liquidjava Public
VS Code extension for LiquidJava - real-time refinement type checking with LSP integration
- liquidjava Public
Refinement type checker for Java with liquid types and typestates - catch bugs at compile time
- liquidjava-examples Public
Code examples demonstrating LiquidJava refinement types and typestate verification
People
This organization has no public members. You must be a member to see who’s a part of this organization.
Top languages
Loading…
Most used topics
Loading…