LBT Software

In our research the main properties of interest are the correctness, security, safety, and performance guarantees of software-based systems—for systems where reliability is a must. For meeting these challenges we develop and use advanced analysis tools and prototypes.   Succinct Solver The Succinct Solver is a tool for solving constraints specified in the Alternation-free Least Fixed Point Logic (ALFP) in clausal form, which is an extension of Horn clauses. Download Succinct Solver here...

LySaTool LySaTool is an automated tool for verifying security properties of protocols that use cryptography to protect network communication from tampering by malicious parties. Protocols modelled in the process calculus LySa are input to the tool. The LySaTool performs a fully automated program analysis that can guarantee confidentiality and authentication properties.   Download LySaTool here...