Serdar Tasiran

Publication Activity (10 Years)

Years Active: 1994-2021
Publications (10 Years): 20

Top Topics

Correctness Criteria

Formal Verification

Concurrent Programs

Temporal Properties

Top Venues

Int. J. Softw. Tools Technol. Transf.

Publications

Byron Cook, Kareem Khazem, Daniel Kroening, Serdar Tasiran, Michael Tautschnig, Mark R. Tuttle
Model checking boot code from AWS data centers. Formal Methods Syst. Des. 57 (1) (2021)
Nathan Chong, Byron Cook, Jonathan Eidelman, Konstantinos Kallas, Kareem Khazem, Felipe R. Monteiro, Daniel Schwartz-Narbonne, Serdar Tasiran, Michael Tautschnig, Mark R. Tuttle
Code-level model checking in the software development workflow at Amazon Web Services. Softw. Pract. Exp. 51 (4) (2021)
James Bornholt, Rajeev Joshi, Vytautas Astrauskas, Brendan Cully, Bernhard Kragl, Seth Markle, Kyle Sauri, Drew Schleit, Grant Slatton, Serdar Tasiran, Jacob Van Geffen, Andrew Warfield
Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3. SOSP (2021)
Martin Kellogg, Martin Schäf, Serdar Tasiran, Michael D. Ernst
Continuous Compliance. ASE (2020)
Nathan Chong, Byron Cook, Konstantinos Kallas, Kareem Khazem, Felipe R. Monteiro, Daniel Schwartz-Narbonne, Serdar Tasiran, Michael Tautschnig, Mark R. Tuttle
Code-level model checking in the software development workflow. ICSE (SEIP) (2020)
Suha Orhun Mutluergil, Serdar Tasiran
A mechanized refinement proof of the Chase-Lev deque using a proof system. Computing 101 (1) (2019)
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Matthew Campagna, Ernie Cohen, Benjamin Grégoire, Vitor Pereira, Bernardo Portela, Pierre-Yves Strub, Serdar Tasiran
A Machine-Checked Proof of Security for AWS Key Management Service. IACR Cryptol. ePrint Arch. 2019 (2019)
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Matthew Campagna, Ernie Cohen, Benjamin Grégoire, Vitor Pereira, Bernardo Portela, Pierre-Yves Strub, Serdar Tasiran
A Machine-Checked Proof of Security for AWS Key Management Service. CCS (2019)
Konstantinos Athanasiou, Byron Cook, Michael Emmi, Colm MacCárthaigh, Daniel Schwartz-Narbonne, Serdar Tasiran
SideTrail: Verifying Time-Balancing of Cryptosystems. VSTTE (2018)
Andrey Chudnov, Nathan Collins, Byron Cook, Joey Dodds, Brian Huffman, Colm MacCárthaigh, Stephen Magill, Eric Mertens, Eric Mullen, Serdar Tasiran, Aaron Tomb, Eddy Westbrook
Continuous Formal Verification of Amazon s2n. CAV (2) (2018)
David R. Cok, Serdar Tasiran
Practical Methods for Reasoning About Java 8's Functional Programming Features. VSTTE (2018)
Hassan Salehe Matar, Erdal Mutlu, Serdar Tasiran, Didem Unat
Output nondeterminism detection for programming models combining dataflow with shared memory. Parallel Comput. 71 (2018)
Ahmed Bouajjani, Constantin Enea, Suha Orhun Mutluergil, Serdar Tasiran
Reasoning About TSO Programs Using Reduction and Abstraction. CAV (2) (2018)
Byron Cook, Kareem Khazem, Daniel Kroening, Serdar Tasiran, Michael Tautschnig, Mark R. Tuttle
Model Checking Boot Code from AWS Data Centers. CAV (2) (2018)
Ahmed Bouajjani, Constantin Enea, Suha Orhun Mutluergil, Serdar Tasiran
Reasoning About TSO Programs Using Reduction and Abstraction. CoRR (2018)
Ahmed Bouajjani, Michael Emmi, Constantin Enea, Burcu Kulahcioglu Ozkan, Serdar Tasiran
Verifying Robustness of Event-Driven Asynchronous Programs Against Concurrency. ESOP (2017)
Talia Ringer, Dan Grossman, Daniel Schwartz-Narbonne, Serdar Tasiran
A solver-aided language for test input generation. Proc. ACM Program. Lang. 1 (OOPSLA) (2017)
Hassan Salehe Matar, Serdar Tasiran, Didem Unat
EmbedSanitizer: Runtime Race Detection Tool for 32-bit Embedded ARM. RV (2017)
Maryam Dabaghchian, Zvonimir Rakamaric, Burcu Kulahcioglu Ozkan, Erdal Mutlu, Serdar Tasiran
Consistency-Aware Scheduling for Weakly Consistent Programs. ACM SIGSOFT Softw. Eng. Notes 42 (4) (2017)
Suha Orhun Mutluergil, Serdar Tasiran
A Mechanized Refinement Proof of the Chase-Lev Deque Using a Proof System. NETYS (2016)
Burcu Kulahcioglu Ozkan, Michael Emmi, Serdar Tasiran
Systematic Asynchrony Bug Exploration for Android Apps. CAV (1) (2015)
Erdal Mutlu, Serdar Tasiran, Benjamin Livshits
Detecting JavaScript races that matter. ESEC/SIGSOFT FSE (2015)
Ali Sezgin, Serdar Tasiran
Moving Around: Lipton's Reduction for TSO - (Regular Submission). VSTTE (2015)
Chris Hawblitzel, Erez Petrank, Shaz Qadeer, Serdar Tasiran
Automated and Modular Refinement Reasoning for Concurrent Programs. CAV (2) (2015)
Gokcen Kestor, Osman S. Unsal, Adrián Cristal, Serdar Tasiran
TRADE: Precise Dynamic Race Detection for Scalable Transactional Memory Systems. ACM Trans. Parallel Comput. 2 (2) (2015)
Burcu Kulahcioglu Ozkan, Erdal Mutlu, Serdar Tasiran
Towards verifying eventually consistent applications. PaPEC@EuroSys (2014)
Erdal Mutlu, Vladimir Gajinov, Adrián Cristal, Serdar Tasiran, Osman S. Unsal
Dynamic Verification for Hybrid Concurrent Programming Models. RV (2014)
Erdal Mutlu, Serdar Tasiran, Benjamin Livshits
I Know It When I See It: Observable Races in JavaScript Applications. Dyla@PLDI (2014)
Gokcen Kestor, Osman S. Unsal, Adrián Cristal, Serdar Tasiran
T-Rex: a dynamic race detection tool for C/C++ transactional memory applications. EuroSys (2014)
Michael Emmi, Burcu Kulahcioglu Ozkan, Serdar Tasiran
Exploiting synchronization in the analysis of shared-memory asynchronous programs. SPIN (2014)
Shaz Qadeer, Serdar Tasiran
Runtime verification of concurrency-specific correctness criteria. Int. J. Softw. Tools Technol. Transf. 14 (3) (2012)
Serdar Tasiran, M. Erkan Keremoglu, Kivanç Muslu
Location pairs: a test coverage metric for shared-memory concurrent programs. Empir. Softw. Eng. 17 (3) (2012)
Tayfun Elmas, Shaz Qadeer, Serdar Tasiran
Goldilocks: a race-aware Java runtime. Commun. ACM 53 (11) (2010)
Oleg Sokolsky, Serdar Tasiran
Editorial. J. Log. Comput. 20 (3) (2010)
Alp Arslan Bayrakci, Alper Demir, Serdar Tasiran
Fast Monte Carlo Estimation of Timing Yield With Importance Sampling and Transistor-Level Circuit Simulation. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 29 (9) (2010)
Tayfun Elmas, Shaz Qadeer, Ali Sezgin, Omer Subasi, Serdar Tasiran
Simplifying Linearizability Proofs with Reduction and Abstraction. TACAS (2010)
Ali Sezgin, Serdar Tasiran, Shaz Qadeer
Tressa: Claiming the Future. VSTTE (2010)
Ali Sezgin, Serdar Tasiran, Kivanç Muslu, Shaz Qadeer
Run-Time Verification of Optimistic Concurrency. RV (2010)
Tayfun Elmas, Ali Sezgin, Serdar Tasiran, Shaz Qadeer
An annotation assistant for interactive debugging of programs with common synchronization idioms. PADTAD (2009)
Serdar Tasiran, Ali Sezgin, Shaz Qadeer
Verifying Optimistic Concurrency: Prophecy Variables and Backward Reasoning. Design and Validation of Concurrent Systems (2009)
Tayfun Elmas, Shaz Qadeer, Serdar Tasiran
A calculus of atomic actions. POPL (2009)
Soner Yaldiz, Alper Demir, Serdar Tasiran
Stochastic Modeling and Optimization for Energy Management in Multicore Systems: A Video Decoding Case Study. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 27 (7) (2008)
Alp Arslan Bayrakci, Alper Demir, Serdar Tasiran
Fast Monte Carlo Estimation of Timing Yield: Importance Sampling with Stochastic Logical Effort (ISLE) CoRR (2008)
Nesra Yannier, Cagatay Basdogan, Serdar Tasiran, Omer Lutfi Sen
Using Haptics to Convey Cause-and-Effect Relations in Climate Visualization. IEEE Trans. Haptics 1 (2) (2008)
Serdar Tasiran, Tayfun Elmas
Rollback Atomicity. RV (2007)
Tayfun Elmas, Shaz Qadeer, Serdar Tasiran
Goldilocks: a race and transaction-aware java runtime. PLDI (2007)
M. Erkan Keremoglu, Serdar Tasiran, Tayfun Elmas
A classification of concurrency bugs in java benchmarks by developer intent. PADTAD (2006)
Tayfun Elmas, Serdar Tasiran
VyrdMC: Driving Runtime Refinement Checking with Model Checkers. Electron. Notes Theor. Comput. Sci. 144 (4) (2006)
Tayfun Elmas, Shaz Qadeer, Serdar Tasiran
Goldilocks: Efficiently Computing the Happens-Before Relation Using Locksets. FATES/RV (2006)
Serdar Tasiran, Tayfun Elmas, Guven Bolukbasi, M. Erkan Keremoglu
A Novel Test Coverage Metric for Concurrently-Accessed Software Components. FATES (2005)
Soner Yaldiz, Alper Demir, Serdar Tasiran, Paolo Ienne, Yusuf Leblebici
Characterizing and Exploiting Task-Load Variability and Correlation for Energy Management in multi-core systems. ESTIMedia (2005)
Tayfun Elmas, Serdar Tasiran, Shaz Qadeer
VYRD: verifYing concurrent programs by runtime refinement-violation detection. PLDI (2005)
Serdar Tasiran, Shaz Qadeer
Runtime Refinement Checking of Concurrent Data Structures. Electron. Notes Theor. Comput. Sci. 113 (2005)
Serdar Tasiran, Yuan Yu, Brannon Batson
Linking Simulation with Formal Verification at a Higher Level. IEEE Des. Test Comput. 21 (6) (2004)
Serdar Tasiran, Yuan Yu, Brannon Batson
Using a formal specification and a model checker to monitor and direct simulation. DAC (2003)
Tamara Munzner, François Guimbretière, Serdar Tasiran, Li Zhang, Yunhong Zhou
TreeJuxtaposer: scalable tree comparison using Focus+Context with guaranteed visibility. ACM Trans. Graph. 22 (3) (2003)
Rajeev Joshi, Leslie Lamport, John Matthews, Serdar Tasiran, Mark R. Tuttle, Yuan Yu
. Formal Methods Syst. Des. 22 (2) (2003)
Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani, Serdar Tasiran
An assume-guarantee rule for checking simulation. ACM Trans. Program. Lang. Syst. 24 (1) (2002)
Shaz Qadeer, Serdar Tasiran
Promising Directions in Hardware Design Verification (invited). ISQED (2002)
Serdar Tasiran, Farzan Fallah, David G. Chinnery, Scott J. Weber, Kurt Keutzer
A Functional Validation Technique: Biased-Random Simulation Guided by Observability-Based Coverage. ICCD (2001)
Serdar Tasiran, Kurt Keutzer
Coverage Metrics for Functional Validation of Hardware Designs. IEEE Des. Test Comput. 18 (4) (2001)
Ellen Sentovich, David L. Dill, Serdar Tasiran
Formal verification meets simulation (tutorial abstract). ICCAD (1999)
Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani, Serdar Tasiran
An Assume-Guarantee Rule for Checking Simulation. FMCAD (1998)
Rajeev Alur, Thomas A. Henzinger, Freddy Y. C. Mang, Shaz Qadeer, Sriram K. Rajamani, Serdar Tasiran
MOCHA: Modularity in Model Checking. CAV (1998)
Serdar Tasiran, Robert K. Brayton
STARI: A Case Study in Compositional and Hierarchical Timing Verification. CAV (1997)
Serdar Tasiran, Rajeev Alur, Robert P. Kurshan, Robert K. Brayton
Verifying Abstractions of Timed Systems. CONCUR (1996)
Serdar Tasiran, Ramin Hojati, Robert K. Brayton
-automata. CHARME (1995)
Adnan Aziz, Serdar Tasiran, Robert K. Brayton
BDD Variable Ordering for Interacting Finite State Machines. DAC (1994)
Adnan Aziz, Felice Balarin, Szu-Tsung Cheng, Ramin Hojati, Timothy Kam, Sriram C. Krishnan, Rajeev K. Ranjan, Thomas R. Shiple, Vigyan Singhal, Serdar Tasiran, Huey-Yih Wang, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli
HSIS: A BDD-Based Environment for Formal Verification. DAC (1994)