BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
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 DBLP: Atig:Mohamed_Faouzi

Contributed to:

CAV 20152015
ESOP 20152015
TACAS 20152015
CAV 20142014
LATA 20142014
CSL-LICS 20142014
DLT 20132013
DLT 20132014
TACAS 20132013
CAV 20122012
ESOP 20122012
LATA 20122012
LICS 20122012
SAS 20122012
TACAS 20122012
CAV 20112011
POPL 20102010
CIAA 20092009
TACAS 20092009
DLT 20082008
CAV (2) 20162016
OOPSLA 20182018
OOPSLA 20192019
PLDI 20172017
PLDI 20192019
POPL 20202020

Wrote 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.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.