default search action
Serdar Tasiran
Person information
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2024
- [e5]Andrew Reynolds, Serdar Tasiran:
Verified Software. Theories, Tools and Experiments - 15th International Conference, VSTTE 2023, Ames, IA, USA, October 23-24, 2023, Revised Selected Papers. Lecture Notes in Computer Science 14095, Springer 2024, ISBN 978-3-031-66063-4 [contents] - 2021
- [j19]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): 34-52 (2021) - [j18]Nathan Chong
, Byron Cook, Jonathan Eidelman, Konstantinos Kallas, Kareem Khazem, Felipe R. Monteiro
Code-level model checking in the software development workflow at Amazon Web Services. Softw. Pract. Exp. 51(4): 772-797 (2021) - [c46]James Bornholt, Rajeev Joshi, Vytautas Astrauskas, Brendan Cully, Bernhard Kragl
Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3. SOSP 2021: 836-850 - 2020
- [c45]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: 11-20 - [c44]Martin Kellogg
Continuous Compliance. ASE 2020: 511-523
2010 – 2019
- 2019
- [j17]Suha Orhun Mutluergil
A mechanized refinement proof of the Chase-Lev deque using a proof system. Computing 101(1): 59-74 (2019) - [c43]José Bacelar Almeida
A Machine-Checked Proof of Security for AWS Key Management Service. CCS 2019: 63-78 - [e4]Isil Dillig, Serdar Tasiran:
Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I. Lecture Notes in Computer Science 11561, Springer 2019, ISBN 978-3-030-25539-8 [contents] - [e3]Isil Dillig, Serdar Tasiran:
Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II. Lecture Notes in Computer Science 11562, Springer 2019, ISBN 978-3-030-25542-8 [contents] - [i4]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: 1042 (2019) - 2018
- [j16]Hassan Salehe Matar, Erdal Mutlu
Output nondeterminism detection for programming models combining dataflow with shared memory. Parallel Comput. 71: 42-57 (2018) - [c42]Ahmed Bouajjani, Constantin Enea, Suha Orhun Mutluergil, Serdar Tasiran:
Reasoning About TSO Programs Using Reduction and Abstraction. CAV (2) 2018: 336-353 - [c41]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: 430-446 - [c40]Byron Cook, Kareem Khazem, Daniel Kroening
Model Checking Boot Code from AWS Data Centers. CAV (2) 2018: 467-486 - [c39]Konstantinos Athanasiou, Byron Cook, Michael Emmi, Colm MacCárthaigh, Daniel Schwartz-Narbonne, Serdar Tasiran:
SideTrail: Verifying Time-Balancing of Cryptosystems. VSTTE 2018: 215-228 - [c38]David R. Cok, Serdar Tasiran:
Practical Methods for Reasoning About Java 8's Functional Programming Features. VSTTE 2018: 267-278 - [i3]Ahmed Bouajjani, Constantin Enea, Suha Orhun Mutluergil, Serdar Tasiran:
Reasoning About TSO Programs Using Reduction and Abstraction. CoRR abs/1804.05196 (2018) - 2017
- [j15]Talia Ringer, Dan Grossman, Daniel Schwartz-Narbonne, Serdar Tasiran:
A solver-aided language for test input generation. Proc. ACM Program. Lang. 1(OOPSLA): 91:1-91:24 (2017) - [j14]Maryam Dabaghchian, Zvonimir Rakamaric, Burcu Kulahcioglu Ozkan
Consistency-Aware Scheduling for Weakly Consistent Programs. ACM SIGSOFT Softw. Eng. Notes 42(4): 1-5 (2017) - [c37]Ahmed Bouajjani, Michael Emmi, Constantin Enea, Burcu Kulahcioglu Ozkan
Verifying Robustness of Event-Driven Asynchronous Programs Against Concurrency. ESOP 2017: 170-200 - [c36]Hassan Salehe Matar, Serdar Tasiran, Didem Unat
EmbedSanitizer: Runtime Race Detection Tool for 32-bit Embedded ARM. RV 2017: 380-389 - 2016
- [c35]Suha Orhun Mutluergil, Serdar Tasiran:
A Mechanized Refinement Proof of the Chase-Lev Deque Using a Proof System. NETYS 2016: 280-294 - 2015
- [j13]Gokcen Kestor
TRADE: Precise Dynamic Race Detection for Scalable Transactional Memory Systems. ACM Trans. Parallel Comput. 2(2): 11:1-11:23 (2015) - [c34]Chris Hawblitzel, Erez Petrank, Shaz Qadeer, Serdar Tasiran:
Automated and Modular Refinement Reasoning for Concurrent Programs. CAV (2) 2015: 449-465 - [c33]Burcu Kulahcioglu Ozkan
Systematic Asynchrony Bug Exploration for Android Apps. CAV (1) 2015: 455-461 - [c32]Erdal Mutlu
Detecting JavaScript races that matter. ESEC/SIGSOFT FSE 2015: 381-392 - [c31]Ali Sezgin, Serdar Tasiran:
Moving Around: Lipton's Reduction for TSO - (Regular Submission). VSTTE 2015: 165-182 - [p1]Adrián Cristal, Burcu Kulahcioglu Ozkan
Verification Tools for Transactional Programs. Transactional Memory 2015: 283-306 - 2014
- [c30]Burcu Kulahcioglu Ozkan
Towards verifying eventually consistent applications. PaPEC@EuroSys 2014: 11:1-11:4 - [c29]Gokcen Kestor
T-Rex: a dynamic race detection tool for C/C++ transactional memory applications. EuroSys 2014: 20:1-20:12 - [c28]Erdal Mutlu
I Know It When I See It: Observable Races in JavaScript Applications. Dyla@PLDI 2014: 1:1-1:7 - [c27]Erdal Mutlu
Dynamic Verification for Hybrid Concurrent Programming Models. RV 2014: 156-161 - [c26]Michael Emmi, Burcu Kulahcioglu Ozkan
Exploiting synchronization in the analysis of shared-memory asynchronous programs. SPIN 2014: 20-29 - 2013
- [e2]Shaz Qadeer, Serdar Tasiran:
Runtime Verification, Third International Conference, RV 2012, Istanbul, Turkey, September 25-28, 2012, Revised Selected Papers. Lecture Notes in Computer Science 7687, Springer 2013, ISBN 978-3-642-35631-5 [contents] - 2012
- [j12]Serdar Tasiran, M. Erkan Keremoglu, Kivanç Muslu:
Location pairs: a test coverage metric for shared-memory concurrent programs. Empir. Softw. Eng. 17(3): 129-165 (2012) - [j11]Shaz Qadeer, Serdar Tasiran:
Runtime verification of concurrency-specific correctness criteria. Int. J. Softw. Tools Technol. Transf. 14(3): 291-305 (2012) - 2010
- [j10]Tayfun Elmas, Shaz Qadeer, Serdar Tasiran:
Goldilocks: a race-aware Java runtime. Commun. ACM 53(11): 85-92 (2010) - [j9]Oleg Sokolsky, Serdar Tasiran:
Editorial. J. Log. Comput. 20(3): 649-650 (2010) - [j8]Alp Arslan Bayrakci
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): 1328-1341 (2010) - [c25]Ali Sezgin, Serdar Tasiran, Kivanç Muslu, Shaz Qadeer:
Run-Time Verification of Optimistic Concurrency. RV 2010: 384-398 - [c24]Tayfun Elmas, Shaz Qadeer, Ali Sezgin, Omer Subasi, Serdar Tasiran:
Simplifying Linearizability Proofs with Reduction and Abstraction. TACAS 2010: 296-311 - [c23]Ali Sezgin, Serdar Tasiran, Shaz Qadeer:
Tressa: Claiming the Future. VSTTE 2010: 25-39
2000 – 2009
- 2009
- [c22]Tayfun Elmas, Ali Sezgin, Serdar Tasiran, Shaz Qadeer:
An annotation assistant for interactive debugging of programs with common synchronization idioms. PADTAD 2009 - [c21]Tayfun Elmas, Shaz Qadeer, Serdar Tasiran:
A calculus of atomic actions. POPL 2009: 2-15 - [i2]Serdar Tasiran, Ali Sezgin, Shaz Qadeer:
Verifying Optimistic Concurrency: Prophecy Variables and Backward Reasoning. Design and Validation of Concurrent Systems 2009 - 2008
- [j7]Soner Yaldiz, Alper Demir
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): 1264-1277 (2008) - [j6]Nesra Yannier, Cagatay Basdogan
Using Haptics to Convey Cause-and-Effect Relations in Climate Visualization. IEEE Trans. Haptics 1(2): 130-141 (2008) - [i1]Alp Arslan Bayrakci, Alper Demir
Fast Monte Carlo Estimation of Timing Yield: Importance Sampling with Stochastic Logical Effort (ISLE). CoRR abs/0805.2627 (2008) - 2007
- [c20]Tayfun Elmas, Shaz Qadeer, Serdar Tasiran:
Goldilocks: a race and transaction-aware java runtime. PLDI 2007: 245-255 - [c19]Serdar Tasiran, Tayfun Elmas:
Rollback Atomicity. RV 2007: 188-201 - [e1]Oleg Sokolsky
Runtime Verification, 7th International Workshop, RV 2007, Vancouver, Canada, March 13, 2007, Revised Selected Papers. Lecture Notes in Computer Science 4839, Springer 2007, ISBN 978-3-540-77394-8 [contents] - 2006
- [c18]Tayfun Elmas, Shaz Qadeer, Serdar Tasiran:
Goldilocks: Efficiently Computing the Happens-Before Relation Using Locksets. FATES/RV 2006: 193-208 - [c17]M. Erkan Keremoglu, Serdar Tasiran, Tayfun Elmas:
A classification of concurrency bugs in java benchmarks by developer intent. PADTAD 2006: 23-26 - 2005
- [c16]Soner Yaldiz, Alper Demir
Characterizing and Exploiting Task-Load Variability and Correlation for Energy Management in multi-core systems. ESTIMedia 2005: 135-140 - [c15]Serdar Tasiran, Tayfun Elmas, Guven Bolukbasi, M. Erkan Keremoglu:
A Novel Test Coverage Metric for Concurrently-Accessed Software Components. FATES 2005: 62-71 - [c14]Tayfun Elmas, Serdar Tasiran, Shaz Qadeer:
VYRD: verifYing concurrent programs by runtime refinement-violation detection. PLDI 2005: 27-37 - [c13]Tayfun Elmas, Serdar Tasiran:
VyrdMC: Driving Runtime Refinement Checking with Model Checkers. RV@CAV 2005: 41-56 - 2004
- [j5]Serdar Tasiran, Yuan Yu, Brannon Batson:
Linking Simulation with Formal Verification at a Higher Level. IEEE Des. Test Comput. 21(6): 472-482 (2004) - [c12]Serdar Tasiran, Shaz Qadeer:
Runtime Refinement Checking of Concurrent Data Structures. RV@ETAPS 2004: 163-179 - 2003
- [j4]Rajeev Joshi, Leslie Lamport, John Matthews, Serdar Tasiran, Mark R. Tuttle, Yuan Yu:
Checking Cache-Coherence Protocols with TLA+. Formal Methods Syst. Des. 22(2): 125-131 (2003) - [j3]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): 453-462 (2003) - [c11]Serdar Tasiran, Yuan Yu, Brannon Batson:
Using a formal specification and a model checker to monitor and direct simulation. DAC 2003: 356-361 - 2002
- [j2]Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani, Serdar Tasiran:
An assume-guarantee rule for checking simulation. ACM Trans. Program. Lang. Syst. 24(1): 51-64 (2002) - [c10]Shaz Qadeer, Serdar Tasiran:
Promising Directions in Hardware Design Verification (invited). ISQED 2002: 381-387 - 2001
- [j1]Serdar Tasiran, Kurt Keutzer:
Coverage Metrics for Functional Validation of Hardware Designs. IEEE Des. Test Comput. 18(4): 36-45 (2001) - [c9]Serdar Tasiran, Farzan Fallah, David G. Chinnery
A Functional Validation Technique: Biased-Random Simulation Guided by Observability-Based Coverage. ICCD 2001: 82-88
1990 – 1999
- 1999
- [c8]Ellen Sentovich, David L. Dill, Serdar Tasiran:
Formal verification meets simulation (tutorial abstract). ICCAD 1999: 221 - 1998
- [c7]Rajeev Alur, Thomas A. Henzinger, Freddy Y. C. Mang, Shaz Qadeer, Sriram K. Rajamani, Serdar Tasiran:
MOCHA: Modularity in Model Checking. CAV 1998: 521-525 - [c6]Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani, Serdar Tasiran:
An Assume-Guarantee Rule for Checking Simulation. FMCAD 1998: 421-432 - 1997
- [c5]Serdar Tasiran, Robert K. Brayton:
STARI: A Case Study in Compositional and Hierarchical Timing Verification. CAV 1997: 191-201 - 1996
- [c4]Serdar Tasiran, Rajeev Alur, Robert P. Kurshan, Robert K. Brayton:
Verifying Abstractions of Timed Systems. CONCUR 1996: 546-562 - 1995
- [c3]Serdar Tasiran, Ramin Hojati, Robert K. Brayton:
Language containment of non-deterministic omega-automata. CHARME 1995: 261-277 - 1994
- [c2]Adnan Aziz, Serdar Tasiran, Robert K. Brayton:
BDD Variable Ordering for Interacting Finite State Machines. DAC 1994: 283-288 - [c1]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: 454-459
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-10-07 21:16 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: