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: Roveri:Marco
Contributed to:
201420122011
20112010
2010
2010
2010
20092009
2009
2008
20082007200720062007
2006
20042004
20032002200220011999
199720172019Wrote 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.
- VMCAI-2008-CimattiRST
- 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.
- CAV-2019-CimattiGMRT
- Extending nuXmv with Timed Transition Systems and Timed Temporal Properties (AC, AG, EM, MR, ST), pp. 376–386.