Serdar Tasiran

According to our database, Serdar Tasiran authored at least 65 papers between 1994 and 2021.

Collaborative distances:

• Dijkstra number of two.
• Erdős number of three.

2021

Code-level model checking in the software development workflow at Amazon Web Services.

Nathan Chong, Byron Cook, Jonathan Eidelman, Konstantinos Kallas, Kareem Khazem, Felipe R. Monteiro, Daniel Schwartz-Narbonne, Serdar Tasiran, Michael Tautschnig, Mark R. Tuttle

Softw. Pract. Exp., 2021

Model checking boot code from AWS data centers.

Byron Cook, Kareem Khazem, Daniel Kroening, Serdar Tasiran, Michael Tautschnig, Mark R. Tuttle

Formal Methods Syst. Des., 2021

Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3.

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

Proceedings of the SOSP '21: ACM SIGOPS 28th Symposium on Operating Systems Principles, 2021

2020

Continuous Compliance.

Martin Kellogg, Martin Schäf, Serdar Tasiran, Michael D. Ernst

Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering, 2020

Code-level model checking in the software development workflow.

Nathan Chong, Byron Cook, Konstantinos Kallas, Kareem Khazem, Felipe R. Monteiro, Daniel Schwartz-Narbonne, Serdar Tasiran, Michael Tautschnig, Mark R. Tuttle

Proceedings of the ICSE-SEIP 2020: 42nd International Conference on Software Engineering, Software Engineering in Practice, Seoul, South Korea, 27 June, 2020

2019

A Machine-Checked Proof of Security for AWS Key Management Service.

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Matthew Campagna, Ernie Cohen, Benjamin Grégoire, Vitor Pereira, Bernardo Portela, Pierre-Yves Strub, Serdar Tasiran

IACR Cryptol. ePrint Arch., 2019

A mechanized refinement proof of the Chase-Lev deque using a proof system.

Suha Orhun Mutluergil, Serdar Tasiran

Computing, 2019

2018

Output nondeterminism detection for programming models combining dataflow with shared memory.

Hassan Salehe Matar, Erdal Mutlu, Serdar Tasiran, Didem Unat

Parallel Comput., 2018

Practical Methods for Reasoning About Java 8's Functional Programming Features.

David R. Cok, Serdar Tasiran

Proceedings of the Verified Software. Theories, Tools, and Experiments, 2018

SideTrail: Verifying Time-Balancing of Cryptosystems.

Konstantinos Athanasiou, Byron Cook, Michael Emmi, Colm MacCárthaigh, Daniel Schwartz-Narbonne, Serdar Tasiran

Proceedings of the Verified Software. Theories, Tools, and Experiments, 2018

Continuous Formal Verification of Amazon s2n.

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

Proceedings of the Computer Aided Verification - 30th International Conference, 2018

Reasoning About TSO Programs Using Reduction and Abstraction.

Ahmed Bouajjani, Constantin Enea, Suha Orhun Mutluergil, Serdar Tasiran

Proceedings of the Computer Aided Verification - 30th International Conference, 2018

2017

Consistency-Aware Scheduling for Weakly Consistent Programs.

Maryam Dabaghchian, Zvonimir Rakamaric, Burcu Kulahcioglu Ozkan, Erdal Mutlu, Serdar Tasiran

ACM SIGSOFT Softw. Eng. Notes, 2017

A solver-aided language for test input generation.

Talia Ringer, Dan Grossman, Daniel Schwartz-Narbonne, Serdar Tasiran

Proc. ACM Program. Lang., 2017

EmbedSanitizer: Runtime Race Detection Tool for 32-bit Embedded ARM.

Hassan Salehe Matar, Serdar Tasiran, Didem Unat

Proceedings of the Runtime Verification - 17th International Conference, 2017

Verifying Robustness of Event-Driven Asynchronous Programs Against Concurrency.

Ahmed Bouajjani, Michael Emmi, Constantin Enea, Burcu Kulahcioglu Ozkan, Serdar Tasiran

Proceedings of the Programming Languages and Systems, 2017

2015

TRADE: Precise Dynamic Race Detection for Scalable Transactional Memory Systems.

Gokcen Kestor, Osman S. Unsal, Adrián Cristal, Serdar Tasiran

ACM Trans. Parallel Comput., 2015

Moving Around: Lipton's Reduction for TSO - (Regular Submission).

Ali Sezgin, Serdar Tasiran

Proceedings of the Verified Software: Theories, Tools, and Experiments, 2015

Detecting JavaScript races that matter.

Erdal Mutlu, Serdar Tasiran, Benjamin Livshits

Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering, 2015

Verification Tools for Transactional Programs.

Adrián Cristal, Burcu Kulahcioglu Ozkan, Ernie Cohen, Gokcen Kestor, Ismail Kuru, Osman S. Unsal, Serdar Tasiran, Suha Orhun Mutluergil, Tayfun Elmas

Proceedings of the Transactional Memory. Foundations, Algorithms, Tools, and Applications, 2015

Systematic Asynchrony Bug Exploration for Android Apps.

Burcu Kulahcioglu Ozkan, Michael Emmi, Serdar Tasiran

Proceedings of the Computer Aided Verification - 27th International Conference, 2015

Automated and Modular Refinement Reasoning for Concurrent Programs.

Chris Hawblitzel, Erez Petrank, Shaz Qadeer, Serdar Tasiran

Proceedings of the Computer Aided Verification - 27th International Conference, 2015

2014

Exploiting synchronization in the analysis of shared-memory asynchronous programs.

Michael Emmi, Burcu Kulahcioglu Ozkan, Serdar Tasiran

Proceedings of the 2014 International Symposium on Model Checking of Software, 2014

Dynamic Verification for Hybrid Concurrent Programming Models.

Erdal Mutlu, Vladimir Gajinov, Adrián Cristal, Serdar Tasiran, Osman S. Unsal

Proceedings of the Runtime Verification - 5th International Conference, 2014

I Know It When I See It: Observable Races in JavaScript Applications.

Erdal Mutlu, Serdar Tasiran, Benjamin Livshits

Proceedings of the Workshop on Dynamic Languages and Applications, 2014

Towards verifying eventually consistent applications.

Burcu Kulahcioglu Ozkan, Erdal Mutlu, Serdar Tasiran

Proceedings of the First Workshop on the Principles and Practice of Eventual Consistency, 2014

T-Rex: a dynamic race detection tool for C/C++ transactional memory applications.

Gokcen Kestor, Osman S. Unsal, Adrián Cristal, Serdar Tasiran

Proceedings of the Ninth Eurosys Conference 2014, 2014

2012

Runtime verification of concurrency-specific correctness criteria.

Shaz Qadeer, Serdar Tasiran

Int. J. Softw. Tools Technol. Transf., 2012

Location pairs: a test coverage metric for shared-memory concurrent programs.

Serdar Tasiran, M. Erkan Keremoglu, Kivanç Muslu

Empir. Softw. Eng., 2012

2010

Fast Monte Carlo Estimation of Timing Yield With Importance Sampling and Transistor-Level Circuit Simulation.

Alp Arslan Bayrakci, Alper Demir, Serdar Tasiran

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2010

Editorial.

Oleg Sokolsky, Serdar Tasiran

J. Log. Comput., 2010

Goldilocks: a race-aware Java runtime.

Tayfun Elmas, Shaz Qadeer, Serdar Tasiran

Commun. ACM, 2010

Tressa: Claiming the Future.

Ali Sezgin, Serdar Tasiran, Shaz Qadeer

Proceedings of the Verified Software: Theories, 2010

Simplifying Linearizability Proofs with Reduction and Abstraction.

Tayfun Elmas, Shaz Qadeer, Ali Sezgin, Omer Subasi, Serdar Tasiran

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2010

Run-Time Verification of Optimistic Concurrency.

Ali Sezgin, Serdar Tasiran, Kivanç Muslu, Shaz Qadeer

Proceedings of the Runtime Verification - First International Conference, 2010

2009

A calculus of atomic actions.

Tayfun Elmas, Shaz Qadeer, Serdar Tasiran

Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2009

An annotation assistant for interactive debugging of programs with common synchronization idioms.

Tayfun Elmas, Ali Sezgin, Serdar Tasiran, Shaz Qadeer

Proceedings of the 7th Workshop on Parallel and Distributed Systems: Testing, 2009

Verifying Optimistic Concurrency: Prophecy Variables and Backward Reasoning.

Serdar Tasiran, Ali Sezgin, Shaz Qadeer

Proceedings of the Design and Validation of Concurrent Systems, 30.08. - 04.09.2009, 2009

2008

Using Haptics to Convey Cause-and-Effect Relations in Climate Visualization.

Nesra Yannier, Cagatay Basdogan, Serdar Tasiran, Omer Lutfi Sen

IEEE Trans. Haptics, 2008

Stochastic Modeling and Optimization for Energy Management in Multicore Systems: A Video Decoding Case Study.

Soner Yaldiz, Alper Demir, Serdar Tasiran

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2008

Fast Monte Carlo Estimation of Timing Yield: Importance Sampling with Stochastic Logical Effort (ISLE)

Alp Arslan Bayrakci, Alper Demir, Serdar Tasiran

CoRR, 2008

2007

Rollback Atomicity.

Serdar Tasiran, Tayfun Elmas

Proceedings of the Runtime Verification, 7th International Workshop, 2007

Goldilocks: a race and transaction-aware java runtime.

Tayfun Elmas, Shaz Qadeer, Serdar Tasiran

Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, 2007

2006

A classification of concurrency bugs in java benchmarks by developer intent.

M. Erkan Keremoglu, Serdar Tasiran, Tayfun Elmas

Proceedings of the 4th Workshop on Parallel and Distributed Systems: Testing, 2006

Goldilocks: Efficiently Computing the Happens-Before Relation Using Locksets.

Tayfun Elmas, Shaz Qadeer, Serdar Tasiran

Proceedings of the Formal Approaches to Software Testing and Runtime Verification, 2006

2005

VyrdMC: Driving Runtime Refinement Checking with Model Checkers.

Tayfun Elmas, Serdar Tasiran

Proceedings of the Fifth Workshop on Runtime Verification, 2005

VYRD: verifYing concurrent programs by runtime refinement-violation detection.

Tayfun Elmas, Serdar Tasiran, Shaz Qadeer

Proceedings of the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation, 2005

A Novel Test Coverage Metric for Concurrently-Accessed Software Components.

Serdar Tasiran, Tayfun Elmas, Guven Bolukbasi, M. Erkan Keremoglu

Proceedings of the Formal Approaches to Software Testing, 5th International Workshop, 2005

Characterizing and Exploiting Task-Load Variability and Correlation for Energy Management in multi-core systems.

Soner Yaldiz, Alper Demir, Serdar Tasiran, Paolo Ienne, Yusuf Leblebici

Proceedings of the 2005 3rd Workshop on Embedded Systems for Real-Time Multimedia, 2005

2004

Runtime Refinement Checking of Concurrent Data Structures.

Serdar Tasiran, Shaz Qadeer

Proceedings of the Fourth Workshop on Runtime Verification, 2004

Linking Simulation with Formal Verification at a Higher Level.

Serdar Tasiran, Yuan Yu, Brannon Batson

IEEE Des. Test Comput., 2004

2003

TreeJuxtaposer: scalable tree comparison using Focus+Context with guaranteed visibility.

Tamara Munzner, François Guimbretière, Serdar Tasiran, Li Zhang, Yunhong Zhou

ACM Trans. Graph., 2003

Checking Cache-Coherence Protocols with TLA⁺.

Rajeev Joshi, Leslie Lamport, John Matthews, Serdar Tasiran, Mark R. Tuttle, Yuan Yu

Formal Methods Syst. Des., 2003

Using a formal specification and a model checker to monitor and direct simulation.

Serdar Tasiran, Yuan Yu, Brannon Batson

Proceedings of the 40th Design Automation Conference, 2003

2002

An assume-guarantee rule for checking simulation.

Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani, Serdar Tasiran

ACM Trans. Program. Lang. Syst., 2002

Promising Directions in Hardware Design Verification (invited).

Shaz Qadeer, Serdar Tasiran

Proceedings of the 3rd International Symposium on Quality of Electronic Design, 2002

2001

Coverage Metrics for Functional Validation of Hardware Designs.

Serdar Tasiran, Kurt Keutzer

IEEE Des. Test Comput., 2001

A Functional Validation Technique: Biased-Random Simulation Guided by Observability-Based Coverage.

Serdar Tasiran, Farzan Fallah, David G. Chinnery, Scott J. Weber, Kurt Keutzer

Proceedings of the 19th International Conference on Computer Design (ICCD 2001), 2001

1999

Formal verification meets simulation (tutorial abstract).

Ellen Sentovich, David L. Dill, Serdar Tasiran

Proceedings of the 1999 IEEE/ACM International Conference on Computer-Aided Design, 1999

1998

MOCHA: Modularity in Model Checking.

Rajeev Alur, Thomas A. Henzinger, Freddy Y. C. Mang, Shaz Qadeer, Sriram K. Rajamani, Serdar Tasiran

Proceedings of the Computer Aided Verification, 10th International Conference, 1998

1997

STARI: A Case Study in Compositional and Hierarchical Timing Verification.

Serdar Tasiran, Robert K. Brayton

Proceedings of the Computer Aided Verification, 9th International Conference, 1997

1996

Verifying Abstractions of Timed Systems.

Serdar Tasiran, Rajeev Alur, Robert P. Kurshan, Robert K. Brayton

Proceedings of the CONCUR '96, 1996

1995

Language containment of non-deterministic <i>omega</i>-automata.

Serdar Tasiran, Ramin Hojati, Robert K. Brayton

Proceedings of the Correct Hardware Design and Verification Methods, 1995

1994

BDD Variable Ordering for Interacting Finite State Machines.

Adnan Aziz, Serdar Tasiran, Robert K. Brayton

Proceedings of the 31st Conference on Design Automation, 1994

HSIS: A BDD-Based Environment for Formal Verification.

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

Proceedings of the 31st Conference on Design Automation, 1994