Researcher:
Taşıran, Serdar

Profile Picture
ORCID

Job Title

Faculty Member

First Name

Serdar

Last Name

Taşıran

Name

Name Variants

Taşıran, Serdar

Email Address

Birth Date

Filters

2003 - 2009172010 - 201822

Advanced Search

Filter by

Settings

Researcher Of Publications: search.filters.isAuthorOfPublication.f8f73136-3271-4bac-844e-cc00e50a7e68

Search Results

Now showing 1 - 10 of 39
  • Placeholder
    PublicationMetadata only
    A novel test coverage metric for concurrently-accessed software components (A work-in-progress paper)
    (Springer-Verlag Berlin, 2006) N/A; Department of Computer Engineering; N/A; Department of Computer Engineering; Department of Computer Engineering; Taşıran, Serdar; Elmas, Tayfun; Bölükbaşı, Güven; Keremoğlu, M. Erkan; Faculty Member; PhD Student; Undergraduate Student; Reseacher; Department of Computer Engineering; College of Engineering; Graduate School of Sciences and Engineering; College of Engineering, College of Engineering; N/A; N/A; N/A; N/A
    We propose a novel, practical coverage metric called "location pairs" (LP) for concurrently-accessed software components. The LP metric captures well common concurrency errors that lead to atomicity or refinement violations. We describe a software tool for measuring LP coverage and outline an inexpensive application of predicate abstraction and model checking for ruling out infeasible coverage targets.
  • Placeholder
    PublicationMetadata only
    Runtime refinement checking of concurrent data structures
    (Elsevier Science Bv, 2005) Qadeer, Shaz; Department of Computer Engineering; Taşıran, Serdar; Faculty Member; Department of Computer Engineering; College of Engineering; N/A
    We present a runtime technique for checking that a concurrent implementation of a data structure conforms to a high-level executable specification with atomic operations. The technique consists of two phases. In the first phase, the implementation code is instrumented in order to record information about its execution into a log. In the second phase, a verification thread runs concurrently with the implementation and uses the logged information to check that the execution conforms to the high-level specification. We pay special attention to reducing the impact of the runtime analysis on the concurrency characteristics and performance of the implementation. We are currently applying our technique to Boxwood [1], a distributed implementation of a B-link tree data structure.
  • Placeholder
    PublicationMetadata only
    Towards verifying eventually consistent applications
    (Association for Computing Machinery, 2014) N/A; N/A; N/A; Department of Computer Engineering; Özkan, Burcu Külahcıoğlu; Mutlu, Erdal; Taşıran, Serdar; PhD Student; PhD Student; Faculty Member; Department of Computer Engineering; Graduate School of Sciences and Engineering; Graduate School of Sciences and Engineering; College of Engineering; N/A; N/A; N/A
    N/A
  • Placeholder
    PublicationMetadata only
    Verification tools for transactional programs
    (Springer, 2015) Cristal, Adrian; Cohen, Ernie; Unsal, Osman; Elmas, Tayfun; N/A; Department of Computer Engineering; N/A; N/A; Özkan, Burcu Külahcıoğlu; Taşıran, Serdar; Mutluergil, Süha Orhun; Kuru, İsmail; PhD Student; Faculty Member; PhD Student; PhD Student; Department of Computer Engineering; Graduate School of Sciences and Engineering; College of Engineering; Graduate School of Sciences and Engineering; Graduate School of Sciences and Engineering; N/A; N/A; N/A; N/A
    While transactional memory has been investigated intensively, its use as a programming primitive by application and system builders is only recently becoming widespread, especially with the availability of hardware support in mainstream commercial CPUs. One key benefit of using transactional memory while writing applications is the simplicity of not having to reason at a low level about synchronization. For this to be possible, verification tools that are aware of atomic blocks and their semantics are needed. While such tools are clearly needed for the adoption of transactional memory in real systems, research in this area is quite preliminary. In this chapter, we provide highlights of our previous work on verification tools for transactional programs.
  • Placeholder
    PublicationMetadata only
    Special issue: international workshop on runtime verification 2007
    (Oxford University Press (OUP), 2010) Sokolsky, Oleg; Department of Computer Engineering; Taşıran, Serdar; Faculty Member; Department of Computer Engineering; College of Engineering; N/A
    N/A
  • Placeholder
    PublicationMetadata only
    Run-time verification of optimistic concurrency
    (Springer, 2010) Qadeer, Shaz; N/A; Department of Computer Engineering; Department of Computer Engineering; Sezgin, Ali; Taşıran, Serdar; Muşlu, Kıvanç; Researcher; Faculty Member; Undergraduate Student; Department of Computer Engineering; N/A; College of Engineering; College of Engineering; N/A; N/A; N/A
    Assertion based specifications are not suitable for optimistic concurrency where concurrent operations are performed assuming no conflict among threads and correctness is cast in terms of the absence or presence of conflicts that happen in the future. What is needed is a formalism that allows expressing constraints about the future. In previous work, we introduced tressa claims and incorporated prophecy variables as one such formalism. We investigated static verification of tressa claims and how tressa claims improve reduction proofs. In this paper, we consider tressa claims in the run-time verification of optimistic concurrency implementations. We formalize, via a simple grammar, the annotation of a program with tressa claims. Our method relieves the user from dealing with explicit manipulation of prophecy variables. We demonstrate the use of tressa claims in expressing complex properties with simple syntax. We develop a run-time verification framework which enables the user to evaluate the correctness of tressa claims. To this end, we first describe the algorithms for monitor synthesis which can be used to evaluate the satisfaction of a tressa claim over a given execution. We then describe our tool implementing these algorithms. We report our initial test results.
  • Placeholder
    PublicationMetadata only
    Stochastic modeling and optimization for energy management in multicore systems: a video decoding case study
    (IEEE-Inst Electrical Electronics Engineers Inc, 2008) Yaldız, Soner; Department of Electrical and Electronics Engineering; Department of Electrical and Electronics Engineering; Demir, Alper; Taşıran, Serdar; Faculty Member; Faculty Member; Department of Electrical and Electronics Engineering; College of Engineering; College of Engineering; 3756; N/A
    This paper presents a novel stochastic modeling and optimization framework for energy minimization in multicore systems running real-time applications with tolerance to deadline misses. This framework is based on stochastic application models, which capture the variability of and the spatial and temporal correlations among the workloads of concurrent and interdependent tasks that constitute the application. These stochastic models are utilized in novel mathematical formulations to obtain optimal energy management policies. Experimental results on MPEG2 video decoding show that significant energy savings can be achieved, often close to the theoretical upper bound.
  • Placeholder
    PublicationMetadata only
    Using haptics to convey cause-and-effect relations in climate visualization
    (IEEE, 2008) Sen, Omer Lutfi; Department of Mechanical Engineering; Department of Computer Engineering; Başdoğan, Çağatay; Taşıran, Serdar; Yannier, Nesra; Faculty Member; Faculty Member; Master Student; Department of Mechanical Engineering; Department of Computer Engineering; College of Engineering; College of Engineering; Graduate School of Sciences and Engineering; 125489; N/A; N/A
    We investigate the potential role of haptics in augmenting the visualization of climate data. In existing approaches to climate visualization, dimensions of climate data such as temperature, humidity, wind, precipitation, and cloud water are typically represented using different visual markers and dimensions such as color, size, intensity, and orientation. Since the numbers of dimensions in climate data are large and climate data need to be represented in connection with the topography, purely visual representations typically overwhelm users. Rather than overloading the visual channel, we investigate an alternative approach in which some of the climate information is displayed through the haptic channel in order to alleviate the perceptual and cognitive load of the user. In this approach, haptic feedback is further used to provide guidance while exploring climate data in order to enable natural and intuitive learning of cause-and-effect relationships between climate variables. As the user explores climate data interactively under the guidance of wind forces displayed by a haptic device, she/he can understand better the occurrence of events such as cloud and rain formation and the effect of climate variables on these events. We designed a set of experiments to demonstrate the effectiveness of this multimodal approach. Our experiments with 33 human subjects show that haptic feedback significantly improves the understanding of climate data and the cause-and-effect relations between climate variables, as well as the interpretation of the variations in climate due to changes in terrain. © 2008 IEEE.
  • Placeholder
    PublicationMetadata only
    A calculus of atomic actions
    (N/A, 2009) Qadeer, Shaz; N/A; Department of Computer Engineering; Elmas, Tayfun; Taşıran, Serdar; PhD Student; Faculty Member; Department of Computer Engineering; Graduate School of Sciences and Engineering; College of Engineering; N/A; N/A
    We present a proof calculus and method for the static verification of assertions and procedure specifications in shared-memory concurrent programs. The key idea in our approach is to use atomicity as a proof tool and to simplify the verification of assertions by rewriting programs to consist of larger atomic actions. We propose a novel, iterative proof style in which alternating use of abstraction and reduction is exploited to compute larger atomic code blocks in a sound manner. This makes possible the verification of assertions in the transformed program by simple sequential reasoning within atomic blocks, or significantly simplified application of existing concurrent program verification techniques such as the Owicki-Gries or rely-guarantee methods. Our method facilitates a clean separation of concerns where at each phase of the proof, the user worries only about only either the sequential properties or the concurrency control mechanisms in the program. We implemented our method in a tool called QED.We demonstrate the simplicity and effectiveness of our approach on a number of benchmarks including ones with intricate concurrency protocols.
  • Placeholder
    PublicationMetadata only
    A classification of concurrency bugs in java benchmarks by developer intent
    (Association for Computing Machinery (ACM), 2006) Department of Computer Engineering; Department of Computer Engineering; N/A; Keremoğlu, M. Erkan; Taşıran, Serdar; Elmas, Tayfun; Researcher; Faculty Member; PhD Student; Department of Computer Engineering; College of Engineering; College of Engineering; Graduate School of Sciences and Engineering; N/A; N/A; N/A
    This work addresses the issue of selecting the formal correctness criterion for a concurrent Java program that best corresponds to the developer's intent. We study a set of concurrency-related bugs detected in Java benchmarks reported in the literature. On these programs, we determine whether race-freedom, atomicity or refinement is the simplest and most appropriate criterion for program correctness. Our purpose is to demonstrate empirically the fact that the appropriate fix for a concurrency error and the selection of a program analysis tool for detecting such an error must be based on the proper expression of the designer's intent using a formal correctness criterion.