BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Travelled to:
1 × Australia
1 × Austria
1 × Canada
1 × China
1 × Denmark
1 × France
1 × New Zealand
1 × Portugal
1 × Taiwan
1 × The Netherlands
1 × United Kingdom
2 × South Africa
3 × Germany
3 × Italy
6 × USA
Collaborated with:
A.Cimatti S.Tonetta M.Pistore R.Bloem A.Griggio R.Sebastiani I.Pill F.Giunchiglia R.Kazhamiakin I.Narasamdya V.Schuppan R.Cavada A.Tchaltsev A.Susi S.Mover A.Micheli E.M.Clarke S.Semprini P.Bertoli M.Bozzano J.Katoen V.Y.Nguyen T.Noll A.Mariotti A.Franzén K.Kalyanasundaram A.Fuxman L.Liu J.Mylopoulos A.Irfan E.Magnago R.Wimmer R.Corvino A.Lazzaro T.Rizzo A.Sanseviero K.Greimel G.Hofferek R.Könighofer R.Seeber A.Chiappini L.Macchi O.Rebollo B.Vittorini E.Giunchiglia A.Tacchella M.Dorigatti C.Mattarei M.Pensallorto
Talks about:
model (9) requir (8) symbol (7) system (6) formal (5) verif (4) valid (4) check (4) tool (4) automata (3)

Person: Marco Roveri

DBLP DBLP: Roveri:Marco

Contributed to:

CAV 20142014
CAV 20122012
CAV 20112011
TACAS 20112011
CAV 20102010
CIAA 20102010
DATE 20102010
ICSE 20102010
ASE 20092009
CAV 20092009
ESEC/FSE 20092009
SEFM 20082008
VMCAI 20082008
CAV 20072007
TACAS 20072007
CIAA 20062006
CIAA 20062007
DAC 20062006
EDOC 20042004
SEFM 20042004
RE 20032003
CAV 20022002
VMCAI 20022002
TACAS 20012001
CAV 19991999
CADE 19971997
CADE 20172017
CAV (1) 20192019

Wrote 30 papers:

CAV-2014-CavadaCDGMMMRT #model checking
The nuXmv Symbolic Model Checker (RC, AC, MD, AG, AM, AM, SM, MR, ST), pp. 334–342.
CAV-2012-CimattiCLNRRST #industrial #validation #verification
Formal Verification and Validation of ERTMS Industrial Railway Train Spacing System (AC, RC, AL, IN, TR, MR, AS, AT), pp. 378–393.
CAV-2011-CimattiGMNR #model checking #named
Kratos — A Software Model Checker for SystemC (AC, AG, AM, IN, MR), pp. 310–316.
TACAS-2011-CimattiNR #abstraction #lazy evaluation #partial order #reduction
Boosting Lazy Abstraction for SystemC with Partial Order Reduction (AC, IN, MR), pp. 341–356.
CAV-2010-BloemCGHKRSS #analysis #named #requirements #synthesis
RATSY — A New Requirements Analysis Tool with Synthesis (RB, AC, KG, GH, RK, MR, VS, RS), pp. 425–429.
CAV-2010-BozzanoCKNNRW #model checking
A Model Checker for AADL (MB, AC, JPK, VYN, TN, MR, RW), pp. 562–565.
CIAA-2010-CimattiMRT #automaton #nondeterminism #regular expression
From Sequential Extended Regular Expressions to NFA with Symbolic Labels (AC, SM, MR, ST), pp. 87–94.
DATE-2010-CimattiFGKR #abstraction #integration #smt
Tighter integration of BDDs and SMT for Predicate Abstraction (AC, AF, AG, KK, MR), pp. 1707–1712.
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.
CAV-2009-CimattiRT #hybrid #requirements #validation
Requirements Validation for Hybrid Systems (AC, MR, ST), pp. 188–203.
ESEC-FSE-2009-BozzanoCRKNN #evaluation #modelling #performance #verification
Verification and performance evaluation of aadl models (MB, AC, MR, JPK, VYN, TN), pp. 285–286.
SEFM-2008-CimattiRST #constraints #modelling
Object Models with Temporal Constraints (AC, MR, AS, ST), pp. 249–258.
Diagnostic Information for Realizability (AC, MR, VS, AT), pp. 52–67.
CAV-2007-BloemCPRT #analysis #formal method #named #requirements
RAT: A Tool for the Formal Analysis of Requirements (RB, RC, IP, MR, AT), pp. 263–267.
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.
CIAA-2006-BloemCPRS #automaton #implementation
Symbolic Implementation of Alternating Automata (RB, AC, IP, MR, SS), pp. 208–218.
CIAA-J-2006-BloemCPR07 #automaton #implementation
Symbolic Implementation of Alternating Automata (RB, AC, IP, MR), pp. 727–743.
DAC-2006-PillSCRBC #analysis #formal method #hardware #requirements
Formal analysis of hardware requirements (IP, SS, RC, MR, RB, AC), pp. 821–826.
EDOC-2004-KazhamiakinPR #framework #process #requirements
A Framework for Integrating Business Processes and Business Requirements (RK, MP, MR), pp. 9–20.
SEFM-2004-KazhamiakinPR #case study #requirements #using #verification #web #web service
Formal Verification of Requirements using SPIN: A Case Study on Web Services (RK, MP, MR), pp. 406–415.
RE-2003-FuxmanLPRM #requirements #specification
Specifying and Analyzing Early Requirements: Some Experimental Results (AF, LL, MP, MR, JM), p. 105–?.
CAV-2002-CimattiCGGPRST #model checking
NuSMV 2: An OpenSource Tool for Symbolic Model Checking (AC, EMC, EG, FG, MP, MR, RS, AT), pp. 359–364.
VMCAI-2002-CimattiPRS #encoding #ltl #model checking #satisfiability
Improving the Encoding of LTL Model Checking into SAT (AC, MP, MR, RS), pp. 196–207.
TACAS-2001-CimattiRB #automaton #model checking #set
Searching Powerset Automata by Combining Explicit-State and Symbolic Model Checking (AC, MR, PB), pp. 313–327.
CAV-1999-CimattiCGR #named #verification
NUSMV: A New Symbolic Model Verifier (AC, EMC, FG, MR), pp. 495–499.
CADE-1997-GiunchigliaRS #logic #testing
A New Method for Testing Decision Procedures in Modal Logics (FG, MR, RS), pp. 264–267.
CADE-2017-CimattiGIRS #incremental #satisfiability
Satisfiability Modulo Transcendental Functions via Incremental Linearization (AC, AG, AI, MR, RS), pp. 95–113.
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.