Join the webinar at https://cesnet.zoom.us/j/93706637432
The VASSAL project organises an online demo webinar focused on recent advances in formal methods, automated analysis and verification. Nine researchers and industry experts will present current approaches and results in methods for improving the reliability, security, and correctness of complex systems.
This event offers an opportunity to explore state-of-the-art techniques shaping the future of critical system design. The programme covers topics including software correctness, hardware verification, model checking, theorem proving, and program analysis.
The webinar is intended for participants with a background or active interest in formal methods, offering a technical perspective on ongoing research and innovation in the field.
| Time | Session | Speaker |
|---|---|---|
| 9:00 - 9:05 | Welcome & Introduction | Milan Ceska (BUT) |
| 9:05 - 9:20 | Brushing off the Rust: Towards Compositional Memory Safety Verification for unsafe Rust presenting the work on a prototype tool that enables automatic, push-button verification of memory safety in unsafe Rust programs and extraction of requirements for memory safety of single functions. | Florian Sextl (TUW) |
| 9:20 - 9:35 | ProofAtlas: A framework for neural clause selection presenting the novel framework for neural given-clause selection and initial results in modern FOL theorem provers. | Alexander Pluska (TUW) |
| 9:35 - 9:50 | POPACheck: A Model Checker for Probabilistic Pushdown Automata presenting the demo of the tool POPACheck: A Model Checker for Probabilistic Pushdown Automata. | Francesco Pontiggia (TUW) |
| 9:50 - 10:05 | Neuro-Symbolic Planning under Uncertainty presenting the novel robust neuro-symbolic planning loop using novel techniques for recurrent policy quantization. | David Hudak (BUT) |
| 10:05 - 10:10 | Break | |
| 10:10 - 10:25 | Parameterized Verification of Quantum Circuits presenting the first fully automatic framework for verifying relational properties of parameterized quantum programs, i.e., programs that, given an input size, generate corresponding quantum circuits. | Ondra Lengal (BUT) |
| 10:25 - 10:40 | When the Past Doesn't Matter: The History Collapse Principle for Bounded-Memory Lazy Matching presenting the ECLEAPS - a novel lazy matching algorithm that is designed to be suitable for executing high-level rule-based control programs of critical real-time continuously-running systems, e.g., from the automotive, aerospace, or healthcare domains. | Jiří Pavela (BUT) |
| 10:40 - 10:55 | SEAL: Symbolic Execution with Separation Logic presenting the SEAL -- a novel static analyser for the verification of programs that manipulate unbounded linked data structures using separation logic to represent abstract memory states. | Tomáš Dacík (BUT) |
| 10:55 - 11:10 | Extraction of information from NL to Formal Language presenting an extraction of formal models from natural language using abstraction refinement. | Sally Ismail (CEA) |
| 11:10 - 11:25 | SMT-based Analysis of MATLAB/Simulink Models presenting a new infrastructure for SMT-based analysis of MATLAB/Simulink models and its future integration into Honeywell's development workflows. | Jan Fiedor (Honeywell) |
| 11:25 - 11:30 | Closing remarks |