Travelled to:1 × Austria
1 × Canada
1 × Germany
1 × New Zealand
1 × Portugal
1 × The Netherlands
2 × France
2 × South Africa
2 × United Kingdom
5 × USA
Collaborated with:A.Cimatti M.Roveri S.Mover A.Griggio R.Sebastiani M.Y.Vardi N.Sharygina A.Tsitovich ∅ A.Susi M.Gario M.Dorigatti M.Bozzano C.Mattarei V.Schuppan E.Singerman R.Cavada A.Mariotti A.Micheli D.Kröning C.M.Wintersteiger J.Daniel K.Y.Rozier E.Magnago A.F.Pires D.Jones G.Kimberly T.Petri R.Robinson A.Chiappini L.Macchi O.Rebollo B.Vittorini M.Pensallorto
Talks about:abstract (7) system (7) model (7) check (6) tempor (5) hybrid (5) properti (4) symbol (4) formal (3) design (3)
Person: Stefano Tonetta
DBLP: Tonetta:Stefano
Contributed to:
2015
201520142014
20132011
2010
201020092009
2009
2009
20082007200720052004201620162019Wrote 24 papers:
- CAV-2015-BozzanoCPJKPRT #analysis #design #safety
- Formal Design and Safety Analysis of AIR6110 Wheel Brake System (MB, AC, AFP, DJ, GK, TP, RR, ST), pp. 518–535.
- TACAS-2015-CimattiGMT #hybrid #model checking #named #smt
- HyComp: An SMT-Based Model Checker for Hybrid Systems (AC, AG, SM, ST), pp. 52–67.
- CAV-2014-CavadaCDGMMMRT #model checking
- The nuXmv Symbolic Model Checker (RC, AC, MD, AG, AM, AM, SM, MR, ST), pp. 334–342.
- CAV-2014-CimattiGMT #hybrid #ltl #verification
- Verifying LTL Properties of Hybrid Systems with K-Liveness (AC, AG, SM, ST), pp. 424–440.
- TACAS-2014-BozzanoCGT #component #design #detection #fault #identification #logic #using
- Formal Design of Fault Detection and Identification Components Using Temporal Epistemic Logic (MB, AC, MG, ST), pp. 326–340.
- TACAS-2014-CimattiGMT #abstraction #modulo theories
- IC3 Modulo Theories via Implicit Predicate Abstraction (AC, AG, SM, ST), pp. 46–61.
- ASE-2013-CimattiDT #contract #named #refinement
- OCRA: A tool for checking the refinement of temporal contracts (AC, MD, ST), pp. 702–705.
- CAV-2011-CimattiMT #automaton #hybrid #performance #verification
- Efficient Scenario Verification for Hybrid Automata (AC, SM, ST), pp. 317–332.
- CIAA-2010-CimattiMRT #automaton #nondeterminism #regular expression
- From Sequential Extended Regular Expressions to NFA with Symbolic Labels (AC, SM, MR, ST), pp. 87–94.
- ICSE-2010-ChiappiniCMRRSTV #formal method #set #validation
- Formalization and validation of a subset of the European Train Control System (AC, AC, LM, OR, MR, AS, ST, BV), pp. 109–118.
- ASE-2009-CavadaCMMMMPRST #requirements #validation
- Supporting Requirements Validation: The EuRailCheck Tool (RC, AC, AM, CM, AM, SM, MP, MR, AS, ST), pp. 665–667.
- ASE-2009-KroeningSTTW #named #source code
- Loopfrog: A Static Analyzer for ANSI-C Programs (DK, NS, ST, AT, CMW), pp. 668–670.
- CAV-2009-CimattiRT #hybrid #requirements #validation
- Requirements Validation for Hybrid Systems (AC, MR, ST), pp. 188–203.
- FM-2009-Tonetta #abstraction #model checking
- Abstract Model Checking without Computing the Abstraction (ST), pp. 89–105.
- SAC-2009-SharyginaTT #abstraction #performance #precise #verification
- The synergy of precise and fast abstractions for program verification (NS, ST, AT), pp. 566–573.
- SEFM-2008-CimattiRST #constraints #modelling
- Object Models with Temporal Constraints (AC, MR, AS, ST), pp. 249–258.
- CAV-2007-CimattiRST #abstraction #logic #satisfiability
- Boolean Abstraction for Temporal Logic Satisfiability (AC, MR, VS, ST), pp. 532–546.
- TACAS-2007-CimattiRT #optimisation #verification
- Syntactic Optimizations for PSL Verification (AC, MR, ST), pp. 505–518.
- TACAS-2007-SebastianiTV #abstraction #clustering #refinement
- Property-Driven Partitioning for Abstraction Refinement (RS, ST, MYV), pp. 389–404.
- CAV-2005-SebastianiTV #hybrid #ltl #model checking
- Symbolic Systems, Explicit Properties: On Hybrid Approaches for LTL Symbolic Model Checking (RS, ST, MYV), pp. 350–363.
- CAV-2004-SebastianiSTV #model checking
- GSTE Is Partitioned Model Checking (RS, ES, ST, MYV), pp. 229–241.
- CAV-2016-DanielCGTM #abstraction #infinity
- Infinite-State Liveness-to-Safety via Implicit Abstraction and Well-Founded Relations (JD, AC, AG, ST, SM), pp. 271–291.
- CAV-2016-GarioCMTR #automation #design #model checking #scalability
- Model Checking at Scale: Automated Air Traffic Control Design Space Exploration (MG, AC, CM, ST, KYR), pp. 3–22.
- CAV-2019-CimattiGMRT
- Extending nuXmv with Timed Transition Systems and Timed Temporal Properties (AC, AG, EM, MR, ST), pp. 376–386.