Jacopo Mantovani

dblp:42/3734 · DBLP profile ↗
← Back
6ranked-venue papers
0as first author
0since 2021 · last 2014
—ORCID · none

Domains — the database's venue-derived domains; a paper can count in several

Software engineering, systems software and programming languages · 6Theory of computation · 1

Expertise — from the expertise taxonomy: the topics of the expert's papers under the CCF categories. A weight counts papers with recency: 1 for a paper about the topic, 0.3 when the topic is its context, halved every five years.

Software engineering, system software, and programming languages
1 paper
Program verification · 100%
Network and information security
1 paper
Cryptographic protocols and secure computation · 100%

Topics — the 4 heaviest of 4, each with the papers that count most for it

TopicWeightPapersLastEvidence papers
Program verification › data structure verification
array program verification
0.112007
The eureka tool for software model checking · ASE 2007
Program verification › model checking
software model checking
0.112007
The eureka tool for software model checking · ASE 2007
Program verification › model checking
symbolic model checking
0.112007
The eureka tool for software model checking · ASE 2007
Cryptographic protocols and secure computation
internet security protocols
0.112005
The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications · CAV 2005

Methods — techniques the papers use, named apart from their topics

symbolic model checking · 0.1predicate abstraction · 0.1
YearPublicationVenuePosition
2014 Counterexample-guided abstraction refinement for linear programs with arrays
Alessandro Armando, Massimo Benerecetti, Jacopo Mantovani
Autom. Softw. Eng.3
2009 Bounded model checking of software using SMT solvers instead of SAT solvers
Alessandro Armando, Jacopo Mantovani, Lorenzo Platania
Int. J. Softw. Tools Technol. Transf.2
2007 The eureka tool for software model checking
abstract
We describe EUREKA, a symbolic model checker for Linear Programs with arrays, i.e. programs where variables and array elements range over a numeric domain and expressions involve linear combinations of variables and array elements. This language fragment easily encodes a large class of programs for which, as demonstrated by our experiments, techniques based on predicate abstraction do not apply successfully.
Alessandro Armando, Massimo Benerecetti, Dario Carotenuto, Jacopo Mantovani, Pasquale Spica
ASE4
2007 Abstraction Refinement of Linear Programs with Arrays
Alessandro Armando, Massimo Benerecetti, Jacopo Mantovani
TACAS3
2005 The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications
Alessandro Armando, David A. Basin, Yohan Boichut, Yannick Chevalier, Luca Compagna, Jorge Cuéllar, Paul Hankes Drielsma, Pierre-Cyrille Héam, Olga Kouchnarenko, Jacopo Mantovani, Sebastian Mödersheim, David von Oheimb, Michaël Rusinowitch, Judson Santiago, Mathieu Turuani, Luca Viganò 0001, Laurent Vigneron
CAV10
2004 Software Model Checking Using Linear Constraints
Alessandro Armando, Claudio Castellini, Jacopo Mantovani
ICFEM3