Serdar Tasiran

76 papers A* 12A 4B 8C 1Journal 22Unranked 25
YearRankTypeTitle / Venue / Authors
2025 A* conf
Formally Verified Cloud-Scale Authorization.
ICSE
Aleks Chakarov, Jaco Geldenhuys, Matthew Heck, Michael Hicks, Sam Huang, Georges-Axel Jaloyan, Anjali Joshi, K. Rustan M. Leino, Mikael Mayer, Sean McLaughlin, Akhilesh Mritunjai, Clément Pit-Claudel, Sorawee Porncharoenwase, Florian Rabe, Marianna Rapoport, Giles Reger, Cody Roux, Neha Rungta, Robin Salkeld, Matthias Schlaipfer, Daniel Schoepe, Johanna Schwartzentruber, Serdar Tasiran, Aaron Tomb, Emina Torlak, Jean-Baptiste Tristan, Lucas G. Wagner, Michael W. Whalen, Remy Willems, Tongtong Xiang, Tae Joon Byun, Joshua M. Cohen, Ruijie Fang, Junyoung Jang, Jakob Rath, Hira Taqdees Syeda, Dominik Wagner, Yongwei Yuan
2024 — ed.
Verified Software. Theories, Tools and Experiments - 15th International Conference, VSTTE 2023, Ames, IA, USA, October 23-24, 2023, Revised Selected Papers
VSTTE
Andrew Reynolds, Serdar Tasiran
2021 J jnl
Code-level model checking in the software development workflow at Amazon Web Services.
Softw. Pract. Exp.
Nathan Chong, Byron Cook, Jonathan Eidelman, Konstantinos Kallas, Kareem Khazem, Felipe R. Monteiro, Daniel Schwartz-Narbonne, Serdar Tasiran, Michael Tautschnig, Mark R. Tuttle
2021 J jnl
Model checking boot code from AWS data centers.
Formal Methods Syst. Des.
Byron Cook, Kareem Khazem, Daniel Kroening, Serdar Tasiran, Michael Tautschnig, Mark R. Tuttle
2021 A* conf
Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3.
SOSP
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
2020 — conf
Code-level model checking in the software development workflow.
ICSE (SEIP)
Nathan Chong, Byron Cook, Konstantinos Kallas, Kareem Khazem, Felipe R. Monteiro, Daniel Schwartz-Narbonne, Serdar Tasiran, Michael Tautschnig, Mark R. Tuttle
2020 A* conf
Continuous Compliance.
ASE
Martin Kellogg, Martin Schäf, Serdar Tasiran, Michael D. Ernst
2019 A* conf
A Machine-Checked Proof of Security for AWS Key Management Service.
CCS
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Matthew Campagna, Ernie Cohen, Benjamin Grégoire, Vitor Pereira, Bernardo Portela, Pierre-Yves Strub, Serdar Tasiran
2019 J jnl
A Machine-Checked Proof of Security for AWS Key Management Service.
IACR Cryptol. ePrint Arch.
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Matthew Campagna, Ernie Cohen, Benjamin Grégoire, Vitor Pereira, Bernardo Portela, Pierre-Yves Strub, Serdar Tasiran
2019 J jnl
A mechanized refinement proof of the Chase-Lev deque using a proof system.
Computing
Suha Orhun Mutluergil, Serdar Tasiran
2019 — ed.
Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I
CAV (1)
Isil Dillig, Serdar Tasiran
2019 — ed.
Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II
CAV (2)
Isil Dillig, Serdar Tasiran
2018 — conf
Continuous Formal Verification of Amazon s2n.
CAV (2)
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
2018 — conf
Model Checking Boot Code from AWS Data Centers.
CAV (2)
Byron Cook, Kareem Khazem, Daniel Kroening, Serdar Tasiran, Michael Tautschnig, Mark R. Tuttle
2018 J jnl
Output nondeterminism detection for programming models combining dataflow with shared memory.
Parallel Comput.
Hassan Salehe Matar, Erdal Mutlu, Serdar Tasiran, Didem Unat
2018 — conf
Practical Methods for Reasoning About Java 8's Functional Programming Features.
VSTTE
David R. Cok, Serdar Tasiran
2018 — conf
Reasoning About TSO Programs Using Reduction and Abstraction.
CAV (2)
Ahmed Bouajjani, Constantin Enea, Suha Orhun Mutluergil, Serdar Tasiran
2018 J jnl
Reasoning About TSO Programs Using Reduction and Abstraction.
CoRR
Ahmed Bouajjani, Constantin Enea, Suha Orhun Mutluergil, Serdar Tasiran
2018 — conf
SideTrail: Verifying Time-Balancing of Cryptosystems.
VSTTE
Konstantinos Athanasiou, Byron Cook, Michael Emmi, Colm MacCárthaigh, Daniel Schwartz-Narbonne, Serdar Tasiran
2017 J jnl
A solver-aided language for test input generation.
Proc. ACM Program. Lang.
Talia Ringer, Dan Grossman, Daniel Schwartz-Narbonne, Serdar Tasiran
2017 J jnl
Consistency-Aware Scheduling for Weakly Consistent Programs.
ACM SIGSOFT Softw. Eng. Notes
Maryam Dabaghchian, Zvonimir Rakamaric, Burcu Kulahcioglu Ozkan, Erdal Mutlu, Serdar Tasiran
2017 B conf
EmbedSanitizer: Runtime Race Detection Tool for 32-bit Embedded ARM.
RV
Hassan Salehe Matar, Serdar Tasiran, Didem Unat
2017 A conf
Verifying Robustness of Event-Driven Asynchronous Programs Against Concurrency.
ESOP
Ahmed Bouajjani, Michael Emmi, Constantin Enea, Burcu Kulahcioglu Ozkan, Serdar Tasiran
2016 — conf
A Mechanized Refinement Proof of the Chase-Lev Deque Using a Proof System.
NETYS
Suha Orhun Mutluergil, Serdar Tasiran
2015 — conf
Automated and Modular Refinement Reasoning for Concurrent Programs.
CAV (2)
Chris Hawblitzel, Erez Petrank, Shaz Qadeer, Serdar Tasiran
2015 — conf
Detecting JavaScript races that matter.
ESEC/SIGSOFT FSE
Erdal Mutlu, Serdar Tasiran, Benjamin Livshits
2015 — conf
Moving Around: Lipton's Reduction for TSO - (Regular Submission).
VSTTE
Ali Sezgin, Serdar Tasiran
2015 — conf
Systematic Asynchrony Bug Exploration for Android Apps.
CAV (1)
Burcu Kulahcioglu Ozkan, Michael Emmi, Serdar Tasiran
2015 J jnl
TRADE: Precise Dynamic Race Detection for Scalable Transactional Memory Systems.
ACM Trans. Parallel Comput.
Gokcen Kestor, Osman S. Unsal, Adrián Cristal, Serdar Tasiran
2015 — ch.
Verification Tools for Transactional Programs.
Transactional Memory
Adrián Cristal, Burcu Kulahcioglu Ozkan, Ernie Cohen, Gokcen Kestor, Ismail Kuru, Osman S. Unsal, Serdar Tasiran, Suha Orhun Mutluergil, Tayfun Elmas
2014 B conf
Dynamic Verification for Hybrid Concurrent Programming Models.
RV
Erdal Mutlu, Vladimir Gajinov, Adrián Cristal, Serdar Tasiran, Osman S. Unsal
2014 — conf
Exploiting synchronization in the analysis of shared-memory asynchronous programs.
SPIN
Michael Emmi, Burcu Kulahcioglu Ozkan, Serdar Tasiran
2014 — conf
I Know It When I See It: Observable Races in JavaScript Applications.
Dyla@PLDI
Erdal Mutlu, Serdar Tasiran, Benjamin Livshits
2014 A conf
T-Rex: a dynamic race detection tool for C/C++ transactional memory applications.
EuroSys
Gokcen Kestor, Osman S. Unsal, Adrián Cristal, Serdar Tasiran
2014 — conf
Towards verifying eventually consistent applications.
PaPEC@EuroSys
Burcu Kulahcioglu Ozkan, Erdal Mutlu, Serdar Tasiran
2013 B ed.
Runtime Verification, Third International Conference, RV 2012, Istanbul, Turkey, September 25-28, 2012, Revised Selected Papers
RV
Shaz Qadeer, Serdar Tasiran
2012 J jnl
Location pairs: a test coverage metric for shared-memory concurrent programs.
Empir. Softw. Eng.
Serdar Tasiran, M. Erkan Keremoglu, Kivanç Muslu
2012 J jnl
Runtime verification of concurrency-specific correctness criteria.
Int. J. Softw. Tools Technol. Transf.
Shaz Qadeer, Serdar Tasiran
2010 J jnl
Editorial.
J. Log. Comput.
Oleg Sokolsky, Serdar Tasiran
2010 J jnl
Fast Monte Carlo Estimation of Timing Yield With Importance Sampling and Transistor-Level Circuit Simulation.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst.
Alp Arslan Bayrakci, Alper Demir, Serdar Tasiran
2010 J jnl
Goldilocks: a race-aware Java runtime.
Commun. ACM
Tayfun Elmas, Shaz Qadeer, Serdar Tasiran
2010 B conf
Run-Time Verification of Optimistic Concurrency.
RV
Ali Sezgin, Serdar Tasiran, Kivanç Muslu, Shaz Qadeer
2010 A conf
Simplifying Linearizability Proofs with Reduction and Abstraction.
TACAS
Tayfun Elmas, Shaz Qadeer, Ali Sezgin, Omer Subasi, Serdar Tasiran
2010 — conf
Tressa: Claiming the Future.
VSTTE
Ali Sezgin, Serdar Tasiran, Shaz Qadeer
2009 A* conf
A calculus of atomic actions.
POPL
Tayfun Elmas, Shaz Qadeer, Serdar Tasiran
2009 — conf
An annotation assistant for interactive debugging of programs with common synchronization idioms.
PADTAD
Tayfun Elmas, Ali Sezgin, Serdar Tasiran, Shaz Qadeer
2009 — conf
Verifying Optimistic Concurrency: Prophecy Variables and Backward Reasoning.
Design and Validation of Concurrent Systems
Serdar Tasiran, Ali Sezgin, Shaz Qadeer
2008 J jnl
Fast Monte Carlo Estimation of Timing Yield: Importance Sampling with Stochastic Logical Effort (ISLE)
CoRR
Alp Arslan Bayrakci, Alper Demir, Serdar Tasiran
2008 J jnl
Stochastic Modeling and Optimization for Energy Management in Multicore Systems: A Video Decoding Case Study.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst.
Soner Yaldiz, Alper Demir, Serdar Tasiran
2008 J jnl
Using Haptics to Convey Cause-and-Effect Relations in Climate Visualization.
IEEE Trans. Haptics
Nesra Yannier, Cagatay Basdogan, Serdar Tasiran, Omer Lutfi Sen
2007 A* conf
Goldilocks: a race and transaction-aware java runtime.
PLDI
Tayfun Elmas, Shaz Qadeer, Serdar Tasiran
2007 B conf
Rollback Atomicity.
RV
Serdar Tasiran, Tayfun Elmas
2007 B ed.
Runtime Verification, 7th International Workshop, RV 2007, Vancouver, Canada, March 13, 2007, Revised Selected Papers
RV
Oleg Sokolsky, Serdar Tasiran
2006 — conf
A classification of concurrency bugs in java benchmarks by developer intent.
PADTAD
M. Erkan Keremoglu, Serdar Tasiran, Tayfun Elmas
2006 — conf
Goldilocks: Efficiently Computing the Happens-Before Relation Using Locksets.
FATES/RV
Tayfun Elmas, Shaz Qadeer, Serdar Tasiran
2005 — conf
A Novel Test Coverage Metric for Concurrently-Accessed Software Components.
FATES
Serdar Tasiran, Tayfun Elmas, Guven Bolukbasi, M. Erkan Keremoglu
2005 — conf
Characterizing and Exploiting Task-Load Variability and Correlation for Energy Management in multi-core systems.
ESTIMedia
Soner Yaldiz, Alper Demir, Serdar Tasiran, Paolo Ienne, Yusuf Leblebici
2005 A* conf
VYRD: verifYing concurrent programs by runtime refinement-violation detection.
PLDI
Tayfun Elmas, Serdar Tasiran, Shaz Qadeer
2005 — conf
VyrdMC: Driving Runtime Refinement Checking with Model Checkers.
RV@CAV
Tayfun Elmas, Serdar Tasiran
2004 J jnl
Linking Simulation with Formal Verification at a Higher Level.
IEEE Des. Test Comput.
Serdar Tasiran, Yuan Yu, Brannon Batson
2004 — conf
Runtime Refinement Checking of Concurrent Data Structures.
RV@ETAPS
Serdar Tasiran, Shaz Qadeer
2003 J jnl
Checking Cache-Coherence Protocols with TLA
Formal Methods Syst. Des.
Rajeev Joshi, Leslie Lamport, John Matthews, Serdar Tasiran, Mark R. Tuttle, Yuan Yu
2003 J jnl
TreeJuxtaposer: scalable tree comparison using Focus+Context with guaranteed visibility.
ACM Trans. Graph.
Tamara Munzner, François Guimbretière, Serdar Tasiran, Li Zhang, Yunhong Zhou
2003 A* conf
Using a formal specification and a model checker to monitor and direct simulation.
DAC
Serdar Tasiran, Yuan Yu, Brannon Batson
2002 J jnl
An assume-guarantee rule for checking simulation.
ACM Trans. Program. Lang. Syst.
Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani, Serdar Tasiran
2002 — conf
Promising Directions in Hardware Design Verification (invited).
ISQED
Shaz Qadeer, Serdar Tasiran
2001 C conf
A Functional Validation Technique: Biased-Random Simulation Guided by Observability-Based Coverage.
ICCD
Serdar Tasiran, Farzan Fallah, David G. Chinnery, Scott J. Weber, Kurt Keutzer
2001 J jnl
Coverage Metrics for Functional Validation of Hardware Designs.
IEEE Des. Test Comput.
Serdar Tasiran, Kurt Keutzer
1999 A conf
Formal verification meets simulation (tutorial abstract).
ICCAD
Ellen Sentovich, David L. Dill, Serdar Tasiran
1998 B conf
An Assume-Guarantee Rule for Checking Simulation.
FMCAD
Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani, Serdar Tasiran
1998 A* conf
MOCHA: Modularity in Model Checking.
CAV
Rajeev Alur, Thomas A. Henzinger, Freddy Y. C. Mang, Shaz Qadeer, Sriram K. Rajamani, Serdar Tasiran
1997 A* conf
STARI: A Case Study in Compositional and Hierarchical Timing Verification.
CAV
Serdar Tasiran, Robert K. Brayton
1996 B conf
Verifying Abstractions of Timed Systems.
CONCUR
Serdar Tasiran, Rajeev Alur, Robert P. Kurshan, Robert K. Brayton
1995 — conf
Language containment of non-deterministic
CHARME
Serdar Tasiran, Ramin Hojati, Robert K. Brayton
1994 A* conf
BDD Variable Ordering for Interacting Finite State Machines.
DAC
Adnan Aziz, Serdar Tasiran, Robert K. Brayton
1994 A* conf
HSIS: A BDD-Based Environment for Formal Verification.
DAC
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