BibSLEIGH — Ahmed

Travelled to:

1 × Belgium
1 × Denmark
1 × Germany
1 × Greece
1 × Hungary
1 × India
1 × Korea
1 × Portugal
1 × Switzerland
1 × The Netherlands
18 × USA
2 × Austria
2 × Canada
2 × Estonia
2 × France
2 × Japan
2 × Spain
4 × Italy
4 × United Kingdom

Collaborated with:

C.Enea M.Emmi P.A.Abdulla P.Habermehl T.Touili T.Vojnar M.Sighireanu M.F.Atig J.Hamza A.Annichini R.Robbana J.Esparza ∅ R.Echahed J.Sifakis S.Qadeer R.Meyer E.Asarin B.Jonsson L.Holík Y.Lakhnech C.Dragoi G.Parlato L.Kaati E.Derevenetc J.Fernandez S.Burckhardt M.Musuvathi M.Nilsson S.O.Mutluergil S.Tasiran P.Moro S.Bensalem A.Rezine E.Möhlmann S.Fratani Y.Jurski J.d'Orso L.Boasson A.Muscholl N.Halbwachs S.M.Beillahi G.Calin A.Lal S.Schwoon D.Suwimonteerabuth A.Rogalewicz A.Collomb-Annichini C.Loiseaux K.Ji R.Zennou M.Erradi R.Guerraoui J.Cederberg F.Haziza G.Yorsh A.M.Rabinovich M.Sagiv A.Meyer S.Graf C.Rodríguez B.K.Ozkan M.Bozga R.Iosif

Talks about:

program (18) system (17) analysi (11) verif (10) verifi (8) model (8) check (8) reachabl (7) automata (7) abstract (7)

Person: Ahmed Bouajjani

DBLP: Bouajjani:Ahmed

Facilitated 1 volumes:

Contributed to:

2015

2014

2013

2012

2011

2010

2009

2008

2009

2008

2007

2006

2005

2004

2003

2002

2001

2000

1999

1998

1997

1995

1994

1992

1991

1990

1991

2017

2018

2019

2017

Wrote 66 papers:

FASE-2015-BouajjaniCDM #lazy evaluation #reachability: Lazy TSO Reachability (AB, GC, ED, RM), pp. 267–282.
ICALP-v2-2015-BouajjaniEEH #on the #reachability: On Reducing Linearizability to State Reachability (AB, ME, CE, JH), pp. 95–107.
POPL-2015-BouajjaniEEH #concurrent #refinement: Tractable Refinement Checking for Concurrent Objects (AB, ME, CE, JH), pp. 651–662.
POPL-2014-BouajjaniEH #consistency #replication #verification: Verifying eventual consistency of optimistic replication systems (AB, CE, JH), pp. 285–296.
ESOP-2013-BouajjaniDM #robust: Checking and Enforcing Robustness against TSO (AB, ED, RM), pp. 533–553.
ESOP-2013-BouajjaniEEH #concurrent #source code #specification #verification: Verifying Concurrent Programs against Sequential Specifications (AB, ME, CE, JH), pp. 290–309.
CAV-2012-AtigBEL #detection #parallel #source code #thread: Detecting Fair Non-termination in Multithreaded Programs (MFA, AB, ME, AL), pp. 210–226.
ESOP-2012-AtigBBM #decidability #memory management #modelling #question #what: What’s Decidable about Weak Memory Models? (MFA, AB, SB, MM), pp. 26–46.
POPL-2012-BouajjaniE #analysis #parallel #recursion #source code: Analysis of recursively parallel programs (AB, ME), pp. 203–214.
TACAS-2012-BouajjaniE #analysis #bound #message passing #source code: Bounded Phase Analysis of Message-Passing Programs (AB, ME), pp. 451–465.
VMCAI-2012-BouajjaniDES #abstract domain #automation #infinity #reasoning #source code: Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data (AB, CD, CE, MS), pp. 1–22.
CAV-2011-AtigBP #analysis: Getting Rid of Store-Buffers in TSO Analysis (MFA, AB, GP), pp. 99–115.
ICALP-v2-2011-BouajjaniMM #robust: Deciding Robustness against Total Store Ordering (AB, RM, EM), pp. 428–440.
PLDI-2011-BouajjaniDES #analysis #interprocedural #on the #source code: On inter-procedural analysis of programs with lists and data (AB, CD, CE, MS), pp. 578–589.
SAS-2011-BouajjaniEP #concurrent #on the #source code: On Sequentializing Concurrent Programs (AB, ME, GP), pp. 129–145.
CAV-2010-BouajjaniDERS #bound #invariant #source code #synthesis: Invariant Synthesis for Programs Manipulating Lists with Unbounded Data (AB, CD, CE, AR, MS), pp. 72–88.
POPL-2010-AtigBBM #memory management #modelling #on the #problem #verification: On the verification problem for weak memory models (MFA, AB, SB, MM), pp. 7–18.
TACAS-2009-AtigBQ #analysis #bound #concurrent #source code #thread: Context-Bounded Analysis for Concurrent Programs with Dynamic Creation of Threads (MFA, AB, SQ), pp. 107–123.
CAV-2008-AbdullaBCHR #abstraction #memory management #source code: Monotonic Abstraction for Programs with Dynamic Memory Heaps (PAA, AB, JC, FH, AR), pp. 341–354.
CIAA-2008-AbdullaBHKV #automaton #bisimulation: Composed Bisimulation for Tree Automata (PAA, AB, LH, LK, TV), pp. 212–222.
CIAA-2008-BouajjaniHHTV #automaton #finite #nondeterminism #testing: Antichain-Based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata (AB, PH, LH, TT, TV), pp. 57–67.
CIAA-J-2008-AbdullaBHKV09 #automaton #bisimulation: Composed Bisimulation for Tree Automata (PAA, AB, LH, LK, TV), pp. 685–700.
TACAS-2008-AbdullaBHKV #automaton #simulation: Computing Simulations over Tree Automata (PAA, AB, LH, LK, TV), pp. 93–108.
TACAS-2008-BouajjaniESS #named: SDSIrep: A Reputation System Based on SDSI (AB, JE, SS, DS), pp. 501–516.
CAV-2007-BouajjaniFQ #analysis #bound #parallel #source code #thread: Context-Bounded Analysis of Multithreaded Programs with Dynamic Linked Structures (AB, SF, SQ), pp. 207–220.
TACAS-2007-BouajjaniJS #framework #infinity #network #process #reasoning: A Generic Framework for Reasoning About Dynamic Networks of Infinite-State Processes (AB, YJ, MS), pp. 690–705.
CAV-2006-BouajjaniBHIMV #automaton #source code: Programs with Lists Are Counter Automata (AB, MB, PH, RI, PM, TV), pp. 517–531.
FoSSaCS-2006-YorshRSMB #linked data #logic #open data: A Logic of Reachable Patterns in Linked Data-Structures (GY, AMR, MS, AM, AB), pp. 94–110.
RTA-2006-BouajjaniE #modelling #source code: Rewriting Models of Boolean Programs (AB, JE), pp. 136–150.
SAS-2006-BouajjaniHRV #data type #model checking: Abstract Regular Tree Model Checking of Complex Dynamic Data Structures (AB, PH, AR, TV), pp. 52–70.
RTA-2005-BouajjaniT #on the #process #reachability #set #term rewriting: On Computing Reachability Sets of Process Rewrite Systems (AB, TT), pp. 484–499.
TACAS-2005-BouajjaniHMV #model checking #source code #verification: Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking (AB, PH, PM, TV), pp. 13–29.
CAV-2004-BouajjaniHV #model checking: Abstract Regular Model Checking (AB, PH, TV), pp. 372–386.
CSL-2003-AbdullaBd #game studies: Deciding Monotonic Games (PAA, AB, Jd), pp. 1–14.
CSL-2003-Bouajjani #infinity #verification: Verification of Infinite State Systems (AB), p. 71.
POPL-2003-BouajjaniET #approach #concurrent #source code #static analysis: A generic approach to the static analysis of concurrent programs with procedures (AB, JE, TT), pp. 62–73.
CAV-2002-BouajjaniT #program transformation: Extrapolating Tree Transformations (AB, TT), pp. 539–554.
CAV-2001-AnnichiniBS #analysis #named #reachability: TReX: A Tool for Reachability Analysis of Complex Systems (AA, AB, MS), pp. 368–372.
ICALP-2001-AbdullaBB #effectiveness #queue: Effective Lossy Queue Languages (PAA, LB, AB), pp. 639–651.
ICALP-2001-Bouajjani #infinity #term rewriting #verification: Languages, Rewriting Systems, and Verification of Infinite-State Systems (AB), pp. 24–39.
LICS-2001-AsarinB #hybrid #turing machine: Perturbed Turing Machines and Hybrid Systems (EA, AB), pp. 269–278.
LICS-2001-BouajjaniMT #algorithm #permutation #verification: Permutation Rewriting and Algorithmic Verification (AB, AM, TT), pp. 399–408.
SAS-2001-BouajjaniCLS #automaton #parametricity: Analyzing Fair Parametric Extended Automata (AB, ACA, YL, MS), pp. 335–355.
CAV-2000-AnnichiniAB #parametricity #reasoning: Symbolic Techniques for Parametric Reasoning about Counter and Clock Systems (AA, EA, AB), pp. 419–434.
CAV-2000-BouajjaniJNT #model checking: Regular Model Checking (AB, BJ, MN, TT), pp. 403–418.
CAV-1999-AbdullaABBHL #abstraction #analysis #infinity #reachability #verification: Verification of Infinite-State Systems by Combining Abstraction and Reachability Analysis (PAA, AA, SB, AB, PH, YL), pp. 146–159.
CAV-1999-AbdullaBJN #verification: Handling Global Conditions in Parameterized System Verification (PAA, AB, BJ, MN), pp. 134–145.
TACAS-1999-AbdullaAB #bound #protocol #verification: Symbolic Verification of Lossy Channel Systems: Application to the Bounded Retransmission Protocol (PAA, AA, AB), pp. 208–222.
CAV-1998-AbdullaBJ #analysis #bound #on the fly: On-the-Fly Analysis of Systems with Unbounded, Lossy FIFO Channels (PAA, AB, BJ), pp. 305–318.
ICALP-1997-BouajjaniH #analysis #reachability #set: Symbolic Reachability Analysis of FIFO Channel Systems with Nonregular Sets of Configurations (AB, PH), pp. 560–570.
CAV-1995-BouajjaniLR #automaton #calculus #hybrid #linear: From Duration Calculus To Linear Hybrid Automata (AB, YL, RR), pp. 196–210.
CAV-1995-BouajjaniR #hybrid #linear #subclass #verification: Verifying ω-Regular Properties for a Subclass of Linear Hybrid Systems (AB, RR), pp. 437–450.
LICS-1995-BouajjaniEH #on the #problem #process #verification: On the Verification Problem of Nonregular Properties for Nonregular Processes (AB, RE, PH), pp. 123–133.
POPL-1995-BouajjaniEH #composition #infinity #parallel #process #verification: Verifying Infinite State Processes with Sequential and Parallel Composition (AB, RE, PH), pp. 95–106.
CAV-1994-BouajjaniER #hybrid #linear #using #verification: Verification of Context-Free Timed Systems Using Linear Hybrid Observers (AB, RE, RR), pp. 118–131.
CAV-1992-BensalemBLS #simulation: Property Preserving Simulations (SB, AB, CL, JS), pp. 260–273.
ICALP-1991-BouajjaniFGRS #branch #safety #semantics: Safety for Branching Time Semantics (AB, JCF, SG, CR, JS), pp. 76–92.
CAV-1990-BouajjaniFH #generative: Minimal Model Generation (AB, JCF, NH), pp. 197–203.
ADC-1991-BouajjaniS #finite #verification: Verification for Finite Systems (Extended Abstract) (AB, JS), pp. 55–57.
ESOP-2017-BouajjaniEEOT #concurrent #robust #source code #verification: Verifying Robustness of Event-Driven Asynchronous Programs Against Concurrency (AB, ME, CE, BKO, ST), pp. 170–200.
CAV-2017-BouajjaniEEM #proving #simulation #using: Proving Linearizability Using Forward Simulations (AB, ME, CE, SOM), pp. 542–563.
CAV-2018-BouajjaniEJQ #bound #message passing #on the #source code #verification: On the Completeness of Verifying Message Passing Programs Under Bounded Asynchrony (AB, CE, KJ, SQ), pp. 372–391.
CAV-2018-BouajjaniEMT #abstraction #reasoning #reduction #source code #using: Reasoning About TSO Programs Using Reduction and Abstraction (AB, CE, SOM, ST), pp. 336–353.
CAV-2019-BeillahiBE #robust: Checking Robustness Against Snapshot Isolation (SMB, AB, CE), pp. 286–304.
CAV-2019-ZennouBEE #consistency: Gradual Consistency Checking (RZ, AB, CE, ME), pp. 267–285.
POPL-2017-BouajjaniEGH #consistency #on the #verification: On verifying causal consistency (AB, CE, RG, JH), pp. 626–638.