Travelled to:1 × Czech Republic
1 × Denmark
1 × Estonia
1 × Poland
1 × USA
2 × Canada
2 × France
2 × Portugal
2 × United Kingdom
3 × Italy
Collaborated with:L.Compagna S.Ranise A.Merlo J.Mantovani R.Carbone M.Rusinowitch M.Benerecetti C.Castellini E.Giunchiglia M.Maratea G.Costa F.Alberti P.Ganty A.Smaill I.Green G.Pellegrino Y.Chevalier S.Mödersheim M.Turuani L.Viganò D.Balzarotti D.Carotenuto P.Spica D.A.Basin L.Vigneron G.Bocci G.Chiarelli G.D.Maglie R.Mammoliti J.Cuéllar D.v.Oheimb M.Bouallagui Y.Boichut P.H.Drielsma P.Héam O.Kouchnarenko J.Santiago W.Arsac T.Avanesov M.Barletta A.Calvi A.Cappai G.Erzse S.Frau M.Minea S.E.Ponta M.Rocchetto M.T.Dashti
Talks about:secur (10) protocol (5) analysi (5) base (5) sat (5) procedur (4) model (4) decis (4) autom (4) check (3)
Person: Alessandro Armando
DBLP: Armando:Alessandro
Facilitated 1 volumes:
EdContributed to:
20152014
20132012
2012
2011
20072007
2005
20042005
200320032002
200120011997Wrote 17 papers:
- TACAS-2015-ArmandoBCCMMM #framework #mobile #named #platform #security #static analysis #verification
- SAM: The Static Analysis Module of the MAVERIC Mobile App Security Verification Platform (AA, GB, GC, GC, GDM, RM, AM), pp. 225–230.
- TACAS-2014-ArmandoCC #model checking #named #satisfiability
- SATMC: A SAT-Based Model Checker for Security-Critical Systems (AA, RC, LC), pp. 31–45.
- SAC-2013-ArmandoCM
- Bring your own device, securely (AA, GC, AM), pp. 1852–1858.
- TACAS-2012-ArmandoAABCCCCCCEFMMOPPRRDTV #architecture #automation #framework #platform #security #trust #validation
- The AVANTSSAR Platform for the Automated Validation of Trust and Security of Service-Oriented Architectures (AA, WA, TA, MB, AC, AC, RC, YC, LC, JC, GE, SF, MM, SM, DvO, GP, SEP, MR, MR, MTD, MT, LV), pp. 267–282.
- TAP-2012-ArmandoPCMB #automation #model checking #protocol #security #testing
- From Model-Checking to Automated Testing of Security Protocols: Bridging the Gap (AA, GP, RC, AM, DB), pp. 3–18.
- CADE-2011-AlbertiAR #analysis #automation #named #policy #security
- ASASP: Automated Symbolic Analysis of Security Policies (FA, AA, SR), pp. 26–33.
- ASE-2007-ArmandoBCMS #model checking
- The eureka tool for software model checking (AA, MB, DC, JM, PS), pp. 541–542.
- TACAS-2007-ArmandoBM #abstraction #array #linear #refinement #source code
- Abstraction Refinement of Linear Programs with Arrays (AA, MB, JM), pp. 373–388.
- CAV-2005-ArmandoBBCCCDHKMMORSTVV #automation #internet #protocol #security #validation
- The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications (AA, DAB, YB, YC, LC, JC, PHD, PCH, OK, JM, SM, DvO, MR, JS, MT, LV, LV), pp. 281–285.
- SAT-2004-ArmandoCGM #constraints #difference #satisfiability
- A SAT-based Decision Procedure for the Boolean Combination of Difference Constraints (AA, CC, EG, MM), pp. 166–173.
- SAT-J-2004-ArmandoCGM05 #constraints #difference #satisfiability
- A SAT-Based Decision Procedure for the Boolean Combination of Difference Constraints (AA, CC, EG, MM), pp. 16–29.
- FME-2003-ArmandoCG #analysis #graph #model checking #protocol #satisfiability #security #using
- SAT-Based Model-Checking of Security Protocols Using Planning Graph Analysis (AA, LC, PG), pp. 875–893.
- SAT-2003-ArmandoC #analysis #protocol #satisfiability #security
- Abstraction-Driven SAT-based Analysis of Security Protocols (AA, LC), pp. 257–271.
- CAV-2002-ArmandoBBCCMRTVV #analysis #protocol #security
- The AVISS Security Protocol Analysis Tool (AA, DAB, MB, YC, LC, SM, MR, MT, LV, LV), pp. 349–353.
- CSL-2001-ArmandoRR
- Uniform Derivation of Decision Procedures by Superposition (AA, SR, MR), pp. 513–527.
- IJCAR-2001-ArmandoCR
- System Description: RDL : Rewrite and Decision Procedure Laboratory (AA, LC, SR), pp. 663–669.
- ASE-1997-ArmandoSG #automation #paradigm #recursion #source code #synthesis
- Automatic Synthesis of Recursive Programs: The Proof-Planning Paradigm (AA, AS, IG), pp. 2–9.