|
Our Lab is a part of the Informatics Faculty at the University of Lugano. The Lab was established in 2006 when Prof. Sharygina received a career award from the Tasso Foundation. The Lab projects focus on automated formal verification with a particular interest in software/hardware model checking, information security, static analysis, abstract interpretation, and decision procedures. We create both theoretical frameworks and practical tools to enable sound and scalable verification of industrial-size systems. For questions about the Lab projects contact natasha.sharygina@usi.ch. We have NEW open PhD and Postdoc positions. For more information, contact natasha.sharygina@usi.ch. |
|
_
Latest news
| 2022-08-02 |
Our paper "Split Transition Power Abstraction for Unbounded Safety has been accepted to FMCAD 2022. |
| 2022-08-02 |
Our paper "SolCMC: Solidity Compiler’s Model Checker" has been accepted to CAV 2022. |
| 2022-03-15 |
Our paper "Transition Power Abstractions for Deep Counterexample Detection" has been accepted to TACAS 2022. |
| 2021-10-23 |
Our paper Lookahead in Partitioning SMT has been accepted to Formal Methods in Computer-Aided Design - FMCAD 2021 |
| 2021-10-22 |
Our paper Using linear algebra in decomposition of Farkas interpolants has been accepted to International Journal on Software Tools for Technology Transfer 2021 |
| 2021-06-24 |
Our paper Lattice-based SMT for program verification has been accepted MEMOCODE 2019 |
| 2021-06-24 |
Our paper Exploiting partial variable assignment in interpolation-based model checking has been accepted to Formal Methods in System Design 2019 |
| 2021-03-05 |
Our paper on Theory-Specific Proof Steps Witnessing Correctness of SMT Executions has been accepted to DAC 2021 |
| 2020-10-24 |
Matteo Marescotti defended his PhD thesis "Parallelization and modeling techniques for scalable SMT-based verification" (05.10.2020) |
| 2020-09-21 |
Our paper on Farkas-Based Tree Interpolation has been accepted to SAS 2020 |
| 2020-07-17 |
Our paper on Incremental Verification by SMT-based Summary Repair has been accepted to FMCAD 2020 |
| 2020-07-10 |
Our SMT-solver OpenSMT won the QF_LRA Single Query Track of the SMT competition 2020 |
| 2020-07-10 |
Our paper Accurate Smart Contract Verification through Direct Modelling has been accepted to ISoLA 2020 |
| 2020-02-03 |
Our paper A Cooperative Parallelization Approach for Property-Directed k-Induction has been accepted to VMCAI 2020 |
| 2019-03-26 |
Our work was mentioned in the media. (see Microsoft Research blog) |
| 2019-03-24 |
Our paper SMTS: Distributed, Visualized Constraint Solving has been accepted to LPAR 2018 |
| 2019-03-22 |
Our paper Decomposing Farkas interpolants has been accepted to TACAS 2019 |
| 2018-11-29 |
Our paper Computing Exact Worst-Case Gas Consumption for Smart Contracts has been accepted to ISoLA 2018 |
| 2018-10-23 |
Our paper Lookahead-Based SMT Solving has been accepted to LPAR-22 |
| 2018-09-24 |
Our paper Function Summarization Modulo Theories has been accepted to LPAR 2018 |
| 2018-08-30 |
The result of our joint work with King's College London "Lattice-Based Refinement in BMC" has been accepted to VSTTE 2018 |
| 2017-10-09 |
Our paper "LRA Interpolants from No Man's Land" has been accepted to HVC 2017 |
| 2017-10-09 |
Our paper "Duality-based interpolation for quantifier-free equalities and uninterpreted functions" has been accepted to FMCAD 2017 |
| 2017-06-30 |
Our paper "Theory Refinement for Program Verification" was accepted to the International Conference on Theory and Applications of Satisfiability Testing (SAT '17) |
| 2016-12-23 |
Our paper "HiFrog: SMT-based Function Summarization for Software Verication" has been accepted to TACAS 2017 |
