|
Our Lab is a part of the Informatics Faculty at the University of Lugano. The Lab was established in 2006 when Prof. Sharygina moved from Carnegie Mellon University to the University of Lugano after receiving 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
| 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 |
| 2016-12-22 |
Leonardo de Sá Alt successfully defended his doctoral thesis "Controlled and Effective Interpolation", 2016-12-09 |
| 2016-08-04 |
Our paper "Clause Sharing and Partitioning for Cloud-Based SMT Solving" was accepted to ATVA 2016 |
| 2016-08-04 |
Our paper "Flexible Interpolation for Efficient Model Checking" was accepted to MEMICS 2016 |
| 2016-08-04 |
Our paper "Combining parallel techniques for Cloud-Based SMT Solving" was accepted to PhD-iFM 2016 |
| 2016-04-18 |
Our paper "Property Directed Equivalence via Abstract Simulation" was accepted to CAV 2016 |
| 2016-04-18 |
Our paper "OpenSMT2: An SMT Solver for Multi-Core and Cloud Computing" was accepted to SAT 2016 |
| 2016-01-12 |
Our paper "PVAIR: Partial Variable Assignment InterpolatoR" was accepted to FASE 2016 |
