Travelled to:1 × Australia
1 × Croatia
1 × Italy
1 × Japan
2 × Austria
2 × Estonia
2 × France
3 × Spain
3 × USA
3 × United Kingdom
Collaborated with:P.A.Abdulla A.Bouajjani J.Stenman Y.Chen A.Rezine C.Leonardsson B.Jonsson K.N.Kumar P.Saivasan S.Burckhardt M.Musuvathi T.Touili L.Holík P.Rümmer Tuan Phong Ngo N.T.Phong G.Parlato S.Qadeer B.Bollig P.Habermehl Rojin Rezvan M.Emmi A.Lal Jatin Arora 0002 S.N.Krishna S.Aronis K.F.Sagonas P.Hofman R.Mayr P.Totzke Magnus Lång Konstantinos Sagonas Bui Phi Diep
Talks about:pushdown (6) under (6) model (6) tso (6) program (5) stateless (4) insert (4) verif (4) optim (4) check (4)
Person: Mohamed Faouzi Atig
DBLP: Atig:Mohamed_Faouzi
Contributed to:
2015
2015
20152014
2014
2014
2013201420132012201220122012
201220122011
2010
2009200920082016
20182019
201720192020Wrote 26 papers:
- CAV-2015-AbdullaACHRRS #constraints #named #smt #string
- Norn: An SMT Solver for String Constraints (PAA, MFA, YFC, LH, AR, PR, JS), pp. 462–469.
- ESOP-2015-AbdullaAP #performance
- The Best of Both Worlds: Trading Efficiency and Optimality in Fence Insertion for TSO (PAA, MFA, NTP), pp. 308–332.
- TACAS-2015-AbdullaAAJLS #model checking
- Stateless Model Checking for TSO and PSO (PAA, SA, MFA, BJ, CL, KFS), pp. 353–367.
- CAV-2014-AbdullaACHRRS #constraints #string #verification
- String Constraints for Verification (PAA, MFA, YFC, LH, AR, PR, JS), pp. 150–166.
- LATA-2014-AbdullaAS #automaton #reachability
- Computing Optimal Reachability Costs in Priced Dense-Timed Pushdown Automata (PAA, MFA, JS), pp. 62–75.
- LICS-CSL-2014-AbdullaAHMKT #energy #game studies #infinity
- Infinite-state energy games (PAA, MFA, PH, RM, KNK, PT), p. 10.
- DLT-2013-AtigKS #multi #order
- Adjacent Ordered Multi-Pushdown Systems (MFA, KNK, PS), pp. 58–69.
- DLT-J-2013-AtigKS14 #multi #order
- Adjacent Ordered Multi-Pushdown Systems (MFA, KNK, PS), pp. 1083–1096.
- TACAS-2013-AbdullaACLR #automation #precise
- Memorax, a Precise and Sound Tool for Automatic Fence Insertion under TSO (PAA, MFA, YFC, CL, AR), pp. 530–536.
- 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.
- LATA-2012-AbdullaAS #automaton #low cost #problem #reachability
- The Minimal Cost Reachability Problem in Priced Timed Pushdown Systems (PAA, MFA, JS), pp. 58–69.
- LICS-2012-AbdullaAS #automaton
- Dense-Timed Pushdown Automata (PAA, MFA, JS), pp. 35–44.
- SAS-2012-AbdullaACLR #abstraction #automation #integer #source code
- Automatic Fence Insertion in Integer Programs via Predicate Abstraction (PAA, MFA, YFC, CL, AR), pp. 164–180.
- TACAS-2012-AbdullaACLR
- Counter-Example Guided Fence Insertion under TSO (PAA, MFA, YFC, CL, AR), pp. 204–219.
- CAV-2011-AtigBP #analysis
- Getting Rid of Store-Buffers in TSO Analysis (MFA, AB, GP), pp. 99–115.
- 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.
- CIAA-2009-AtigT #communication #parallel #source code #verification
- Verifying Parallel Programs with Dynamic Communication Structures (MFA, TT), pp. 145–154.
- 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.
- DLT-2008-AtigBH #automaton #multi
- Emptiness of Multi-pushdown Automata Is 2ETIME-Complete (MFA, BB, PH), pp. 121–133.
- CAV-2016-AbdullaAJL #model checking
- Stateless Model Checking for POWER (PAA, MFA, BJ, CL), pp. 134–156.
- OOPSLA-2018-AbdullaAJN #model checking #semantics
- Optimal stateless model checking under the release-acquire semantics (PAA, MFA, BJ, TPN), p. 29.
- OOPSLA-2019-AbdullaAJLNS #consistency #equivalence #model checking
- Optimal stateless model checking for reads-from equivalence under sequential consistency (PAA, MFA, BJ, ML, TPN, KS), p. 29.
- PLDI-2017-AbdullaACDHRR #analysis #constraints #framework #performance #string
- Flatten and conquer: a framework for efficient analysis of string constraints (PAA, MFA, YFC, BPD, LH, AR, PR), pp. 602–617.
- PLDI-2019-AbdullaAAK #semantics #source code #verification
- Verification of programs under the release-acquire semantics (PAA, JA0, MFA, SNK), pp. 1117–1132.
- POPL-2020-AbdullaAR #verification
- Parameterized verification under TSO is PSPACE-complete (PAA, MFA, RR), p. 29.