BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
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 DBLP: Tonetta:Stefano

Contributed to:

CAV 20152015
TACAS 20152015
CAV 20142014
TACAS 20142014
ASE 20132013
CAV 20112011
CIAA 20102010
ICSE 20102010
ASE 20092009
CAV 20092009
FM 20092009
SAC 20092009
SEFM 20082008
CAV 20072007
TACAS 20072007
CAV 20052005
CAV 20042004
CAV (1) 20162016
CAV (2) 20162016
CAV (1) 20192019

Wrote 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.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.