Lightweight Formal Methods for Software Engineering (FORSE)

Today’s software systems are increasingly complex, with high degree of concurrency and distribution. Given their size and complexity, applying formal verification techniques to guarantee their correctness is often impractical.

At the FORSE lab, we aim to bridge the gap between informal testing and full formal verification of software systems using lightweight formal methods. We develop automated software methods that incorporate the rigorous approaches of formal methods, combinatorics, and verification into practical tools for software analysis. Our methods aim to strike a balance between rigorous mathematical reasoning and practical usability by applying formal methods in a less complete and more flexible way to improve software reliability without the full cost and complexity of formal verification.

Our research develops automated software analysis and testing methods for large-scale software systems, including:

• Decentralized consensus systems and blockchains
• Distributed systems with weak consistency and weak isolation
• Service-oriented, microservices architectures
• Shared-memory multicore programs

Related Research Projects:

• “Coverage-directed randomized testing of distributed systems” where we propose test coverage notions and coverage-guided testing methods for distributed systems, awarded with Amazon Research Award (2022).

• “Feedback-guided fault-injection testing of blockchain systems” where we propose automated testing methods for finding fault-tolerance bugs in blockchain systems, awarded with Stellar Academic Research Grant (2023).

Related MSc Courses:

• CS4720 - Research in Program Analysis (since 2025)
• CS4405 - Analysis of Concurrent and Distributed Programs (until 2024)

Contact if you are interested in working on lightweight formal methods, automated reasoning, and software testing for analyzing concurrent and distributed software systems.