This material
is presented to ensure timely dissemination of scholarly and technical work.
Copyright and all rights therein are retained by authors or by other copyright
holders. All persons copying this information are expected to adhere to the
terms and constraints invoked by each author's copyright. In most cases, these
works may not be reposted without the explicit permission of the copyright
holder.
Serdar Tasiran, Shaz Qadeer
Runtime
Verification of Concurrency-Specific Correctness Criteria
International Journal on Software Tools for Technology Transfer (STTT) 14(3),
2012
Serdar Tasiran, M. Erkan Keremoglu, Kivanc Muslu
Location Pairs:
A Test Coverage Metric for Shared-Memory Concurrent Programs
Empirical Software Engineering Journal 17(3),
2012
Omer Subasi,
Tayfun Elmas, Serdar Tasiran
On Justifying and Verifying Relaxed Detection of Conflicts
in Concurrent Programs
WoDet 3: Third Workshop on Determinism and
Correctness in Parallel Programming
Co-located with ASPLOS 12, 17th Intl. Conf. on Architectural Support for
Programming Languages
and Operating Systems, March 3-7, 2012, London, England, UK
Umit Can Bekar, Tayfun Elmas, Semih
Okur, Serdar Tasiran
KUDA: GPU
Accelerated Split Race Checker
WoDet 3: Third Workshop on Determinism and
Correctness in Parallel Programming
Co-located with ASPLOS 12, 17th Intl. Conf. on
Architectural Support for Programming Languages
and Operating Systems, March 3-7, 2012, London, England, UK
Tayfun Elmas, Shaz Qadeer, Serdar
Tasiran
Goldilocks:
A Race- Aware Runtime
Communications of the Association for Computing Machinery (CACM)
Research Highlights Section. November 2010
Ali Sezgin,
Serdar Tasiran, Kıvanc Muslu, Shaz Qadeer.
Run-Time Verification of
Optimistic Concurrency
Intl. Conference on Runtime Verification (RV 2010) Malta, November 1-4, 2010
Ali Sezgin,
Serdar Tasiran, Shaz Qadeer.
Tressa: Claiming the Future.
Verified Software: Theories, Tools and Experiments (VSTTE
2010).
Edinburgh, Scotland. August 16-19, 2010
Simplifying Linearizability Proofs with
Reduction and Abstraction. (Technical
report)
Tayfun Elmas, Shaz Qadeer, Ali Sezgin, Omer Subasi, Serdar Tasiran.
ETAPS 2010 Conference on Tools and Algorithms for the
Construction and Analysis of Systems (TACAS).
Fast Monte Carlo Estimation
of Timing Yield With Importance Sampling and Transistor-Level Circuit
Simulation
Alp Arslan Bayrakci, Alper Demir, Serdar
Tasiran
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
29(9):1328-1341. September 2010.
Shaz Qadeer, Ali Sezgin, Serdar Tasiran
Back
and Forth: Prophecy Variables for Static Verification of Concurrent Programs
Microsoft Research Technical Report, MSR TR-2009-142. October 13, 2009.
Tayfun Elmas, Ali Sezgin, Shaz Qadeer,
Serdar Tasiran
An
Annotation Assistant for Interactive Debugging of Programs with Common
Synchronization Idioms.
In ACM 2009 Workshop on Parallel and Distributed Systems: Testing, Analysis and
Debugging (PADTAD '09)
Chicago, Illionis, USA, July 19-20, 2009.
Tayfun Elmas, Shaz
Qadeer, Serdar Tasiran
A Calculus of Atomic
Actions
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '09)
Full version: Microsoft Research Technical Report, MSR TR-2008-99
Tayfun Elmas, Shaz
Qadeer, Serdar Tasiran
A
Calculus of Atomic Actions
Microsoft Research Technical Report, MSR-TR-2008-99, July 18, 2008
Serdar Tasiran
A
Compositional Method for Verifying Software Transactional Memory
Implementations
Microsoft Research Technical Report, MSR-TR-2008-56, April 10, 2008.
Soner Yaldiz, Alper Demir, Serdar
Tasiran
Stochastic Modeling and Optimization for
Energy Management in Multi-Core Systems: A Video Decoding Case Study
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems,
July 2008
Nesra Yannier, Cagatay Basdogan, Serdar Tasiran, Omer Lutfi Sen
Using Haptics to Convey Cause and Effect Relations in
Climate Visualization
16th Symposium on Haptic Interfaces for Virtual Environments and Teleoperator Systems, March 2008
Held in conjunction with IEEE Virtual Reality
Also in IEEE Transactions on Haptics
Tayfun Elmas, Shaz Qadeer, Serdar
Tasiran
Goldilocks: A Race- and Transaction-Aware
Java Runtime
In Proc. ACM SIGPLAN 2007 Conf. on Programming Language Design and
Implementation,
PLDI '07. June 10-13, 2007.
Also in ACM SIGPLAN Notices, Volume 42, Issue 6, June 2007
Serdar Tasiran, Tayfun Elmas
Rollback Atomicity
Proc. of the 7th Workshop on Runtime Verification (RV 2007)
6th International Conference on Aspect-Oriented Software Development Conference
(AOSD 2007)
Vancouver, BC, Canada, March 2007
Tayfun Elmas, Shaz Qadeer, Serdar
Tasiran
Goldilocks: Efficiently
computing the happens-before relation using locksets
Proceedings of the Workshop on Formal Approaches to Testing and Runtime
Verification (FATES/RV 2006)
Seattle, WA, August 2006
Tayfun Elmas, Shaz Qadeer, Serdar
Tasiran
Precise race detection
and efficient model checking using locksets
Microsoft Research Technical Report, MSR-TR-2005-118, March 2006.
Serdar Tasiran, Alper Demir,
Smart Monte Carlo for Yield
Estimation (Abbreviated
version )
ACM/IEEE International Workshop on Timing
Issues in the Specification and Synthesis of Digital Systems (TAU)
San Jose, CA, Februrary 2006.
Alper Demir, Serdar Tasiran,
Stochastic Logical Effort:Designing for Timing Yield on the Back of an Envelope
(Abbreviated version
)
ACM/IEEE International Workshop on Timing
Issues in the Specification and Synthesis of Digital Systems (TAU)
San Jose, CA, Februrary 2006
Soner Yaldiz, Alper Demir, Serdar
Tasiran, Paolo Ienne, Yusuf
Leblebici
Characterizing and Exploiting
Task-Load Variability and Correlation for Energy Management
IEEE 2005 3rd Workshop on Embedded Systems for Real-Time Multimedia
New York Metropolitan Area, USA. September 22-23, 2005
Serdar Tasiran, Tayfun Elmas, Guven
Bolukbasi, M. Erkan Keremoglu
A Novel Test Coverage
Metric for Concurrently-Accessed Software Components
Fifth
International Workshop on Formal Approaches to Testing of Software (FATES
2005).
University of Edinburgh, Scotland, UK, July 11, 2005
Tayfun Elmas, Serdar Tasiran
VyrdMC:
Driving Runtime Refinement Checking with Model Checkers
Fifth Workshop on Runtime
Verification (RV'05).
The University of Edinburgh, Scotland, UK. July 12,
2005.
Tayfun Elmas, Serdar Tasiran
Koşutzamanlı Yazılım
Bileşenleri için Bir Otomatik Doğrulama
Çerçevesi: VyrdMC
2nd National Software Engineering Symposium.
METU, Ankara, Turkey, September 22-24, 2005.
Tayfun Elmas, Serdar Tasiran, Shaz Qadeer
VYRD: VerifYing
Concurrent Programs by Runtime Refinement-Violation Detection
ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation,
PLDI '05. June 12-15, 2005.
ACM SIGPLAN Notices Vol. 40 No. 6. pp 27-37 (June 2005)
Serdar Tasiran, Yuan Yu,
Brannon Batson
Linking Simulation with Formal Verification
at a Higher Level
IEEE Design and Test of Computers,
Special Issue on Exploring Synergies for Design Verification, Nov-Dec 2004
Serdar Tasiran, Shaz Qadeer
Runtime
Refinement Checking of Concurrent Data Structures
In Proc. RV'04 - Fourth Workshop on Runtime Verification, April 3, 2004,
Barcelona, Spain
The European Joint Conferences on Theory and Practice of Software (ETAPS '04)
Electronic
Notes in Theoretical Computer Science, Elsevier Science
Tamara Munzner,
Francois Guimbretière, Serdar
Tasiran, Li Zhang, Yunhong
Zhou
TreeJuxtaposer: scalable tree comparison using Focus+Context with guaranteed visibility.
ACM Transactions on Graphics (TOG) 22(3): 453-462 (2003)
Special issue: Proceedings of ACM SIGGRAPH 2003
Serdar Tasiran, Yuan Yu,
Brannon Batson
Using a
formal specification and a model checker to monitor and direct simulation.
In Proc. of the 40th ACM/IEEE Design Automation Conference,
DAC03
San Diego, CA, 2003.: 356-361 (Invited talk to ISSCC 2004, Highlights of DAC
Session)
Rajeev Joshi, Leslie Lamport, John Matthews, Serdar Tasiran, Mark R. Tuttle,
Yuan Yu:
Checking Cache-Coherence
Protocols with TLA+.
Formal Methods in System Design 22(2): 125-131 (2003)
Shaz Qadeer, Serdar
Tasiran,
Promising Directions in
Hardware Design Verification (invited).
In Proc. Intl. Symposium on Quality Electronic Design, ISQED '02, San
Jose, CA, 2002.
S. Tasiran,
Y. Yu, R. Joshi, B. Batson, S. Kreider
Using
Formal Specifications to Monitor and Guide Simulation:
Verifying the Cache Coherence Engine of the Alpha 21364 Microprocessor.
Proc. of the IEEE Computer Society Workshop on Microprocessor Test and
Verification, MTV 02,
T.A. Henzinger,
S. Qadeer, S. Rajamani, S. Tasiran
An
assume-guarantee rule for checking simulation
ACM Transactions on Programming Languages and Systems (TOPLAS)
Volume 24 , Issue 1 (January 2002), Pages: 51 - 64
S. Tasiran,
F. Fallah, D. G. Chinnery,
S. J. Weber, K. Keutzer.
Coverage-Directed
Generation Of Biased Random Vectors For Functional Validation
Of Sequential Circuits.
In Proc. of the IEEE/ACM Workshop on Logic and Synthesis, IWLS 01,
Lake Tahoe, CA, 2001, pp. 287-292.
S. Tasiran,
K. Keutzer
Coverage
Metrics For Functional Validation Of Hardware Designs.
IEEE Design and Test of Computers, Vol. 18, No. 4, 2001, pp. 36-45.
S. Tasiran,
F. Fallah, D. G. Chinnery,
S. J. Weber, K. Keutzer
A Functional Validation Technique:
Biased Random Simulation Guided By Observability-Based
Coverage.
In Proc. of the IEEE Intl Conf. on Computer Design: VLSI in Computers &
Processors, ICCD 01,
Austin, TX, 2001, pp. 82-88.
Ellen Sentovich,
David L. Dill, Serdar Tasiran:
Formal
verification meets simulation (tutorial abstract).
Proceedings of the 1999 IEEE/ACM international conference on Computer-aided
design
T.A. Henzinger, S. Qadeer,
S. Rajamani, S. Tasiran
An
Assume-Guarantee Rule for Checking Simulation
In Proc. of the 2nd Intl. Conf. on Formal Methods in
Computer-aided Design, FMCAD '98,
LNCS 1522, Palo Alto, CA, 1998, pp. 421-432.
S. Tasiran,
S.P. Khatri, S. Yovine,
R.K. Brayton, A. Sangiovanni-Vincentelli
A Timed
Automaton-Based Method for Accurate Computation of Circuit Delay
in the Presence of Cross-Talk.
In Proc. of the 2nd Intl. Conf. on Formal Methods in
Computer-aided Design, FMCAD '98,
LNCS 1522, Palo Alto, CA, 1998, pp. 149-166.
R. Alur,
T.A. Henzinger, F.Y.C. Mang,
S. Qadeer, S.K. Rajamani,
S. Tasiran
MOCHA:
Modularity in Model Checking.
In Proc. of the 10th Intl. Conf. on Computer-Aided Verification, CAV '98,
LNCS 1427, Vancouver, Canada, 1998, pp. 521-525.
S. Tasiran,
Y. Kukimoto, R. K. Brayton
Computing
Delay with Coupling Using Timed Automata.
In Proc. of IEEE/ACM Intl. Workshop on Timing Issues in the Specification
and Synthesis of Digital Systems, TAU '97, Austin, TX, 1997.
S. Tasiran,
R. K. Brayton
STARI:
A Case Study in Compositional and Hierarchical Timing Verification.
In Proc. of the 9th Intl. Conf. on Computer-Aided Verification, CAV '97,
LNCS 1254, Haifa, Israel, 1997, pp. 191-201.
S. Tasiran, R. Alur, R. P. Kurshan, R. K. Brayton
Verifying
Abstractions of Timed Systems.
In Proc. of 7th International Conference on Concurrency Theory, CONCUR '96,
LNCS 1119, Pisa, Italy, 1996, pp. 546-562.
S. Tasiran, R. K. Brayton
On Iterative Verification with Timed Automata.
In Proc. of ACM Intl. Workshop on Timing Issues in the Specification and
Synthesis of Digital Systems, TAU '95,
Seattle, WA, 1995.
S. Tasiran,
R. Hojati, R. K. Brayton
Language
Containment Using Non-deterministic Omega-Automata. In Proc. of Advanced
Research Working Conference on Correct Hardware Design and Verification
Methods, CHARME'95,
LNCS 987, Frankfurt, Germany, 1995, pp. 261-277.
A. Aziz, S. Tasiran, R. K. Brayton
BDD
Variable Ordering for Interacting Finite State Machines.
In Proc. of the 31st ACM/IEEE Design Automation
Conference, DAC94
San Diego, CA, 1994.
A. Aziz, F. Balarin, S.-T. Cheng, R. Hojati,
T. Kam, S. Krishnan, R. Ranjan,
T. Shiple, V. Singhal,
S. Tasiran, H.-Y. Wang, R. Brayton,
A. Sangiovanni-Vincentelli
HSIS: A BDD-Based
Environment for Formal Verification.
In Proc. of the 31st ACM/IEEE Design Automation
Conference, DAC94
San Diego, CA, 1994.
A. Aziz, S. Tasiran, R. K. Brayton.
A Communication
Complexity Based Approach to BDD Variable Ordering
for Systems of Interacting Finite State Machines.
In Workshop Notes of ACM/IEEE Intl. Workshop on Logic Synthesis, IWLS93
Tahoe City, CA, 1993.
M. S. Ünlü, S. Strite, A.L. Demirel, S. Tasiran, A. Salvador,
H. Morkoç
Wavelength
Selective Optical Logic and Interconnects.
IEEE Journal on Quantum Electronics, Vol. 29, No. 2, 1993, pp. 411-425.
M. S. Ünlü, A.L. Demirel, S. Strite, S. Tasiran, A. Salvador,
and H. Morkoç
Wavelength Demultiplexing Optical Switch.
Applied Physics Letters, Vol. 60, No. 15, 1992, pp. 1797-1799
Serdar Tasiran
Compositional
and Hierarchical Techniques for the Formal Verification of Real-Time Systems
Ph.D. Thesis, University of California at Berkeley, 1998
Serdar Tasiran
Language Containment Using Non-deterministic w-automata
M.S. Thesis, University of California at Berkeley, 1995