Researcher:
Özkan, Burcu Külahcıoğlu

Profile Picture
ORCID

Job Title

PhD Student

First Name

Burcu Külahcıoğlu

Last Name

Özkan

Name

Name Variants

Özkan, Burcu Külahcıoğlu
Özkan, Burcu

Email Address

Birth Date

Filters

2014 - 20175

Advanced Search

Filter by

Settings

Researcher Of Publications: search.filters.isAuthorOfPublication.335848bc-adf8-4e7d-b0f0-05277fa14f8c

Search Results

Now showing 1 - 5 of 5
  • 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
    Exploiting synchronization in the analysis of shared-memory asynchronous programs
    (Association for Computing Machinery, 2014) Emmi, Michael; N/A; Department of Computer Engineering; Özkan, Burcu Külahcıoğlu; Taşıran, Serdar; PhD Student; Faculty Member; Department of Computer Engineering; Graduate School of Sciences and Engineering; College of Engineering; N/A; N/A
    As asynchronous programming becomes more mainstream, program analyses capable of automatically uncovering programming errors are increasingly in demand. Since asynchronous program analysis is computationally costly, current approaches sacrifice completeness and focus on limited sets of asynchronous task schedules that are likely to expose programming errors. These approaches are based on parameterized task schedulers, each of which admits schedules which are variations of a default deterministic schedule. By increasing the parameter value, a larger variety of schedules is explored, at a higher cost. The efficacy of these approaches depends largely on the default deterministic scheduler on which varying schedules are fashioned. We find that the limited exploration of asynchronous program behaviors can be made more efficient by designing parameterized schedulers which better match the inherent ordering of program events, e.g., arising from waiting for an asynchronous task to complete. We follow a reduction-based sequentialization" approach to analyzing asynchronous programs, which leverages existing (sequential) program analysis tools by encoding asynchronous program executions, according to a particular scheduler, as the executions of a sequential program. Analysis based on our new scheduler comes at no greater computational cost, and provides strictly greater behavioral coverage than analysis based on existing parameterized schedulers; we validate these claims both conceptually, with complexity and behavioral-inclusion arguments, and empirically, by discovering actual reported bugs faster with smaller parameter values.
  • Placeholder
    PublicationMetadata only
    Systematic asynchrony bug exploration for android apps
    (Springer-Verlag Berlin, 2015) Emmi, Michael; N/A; Department of Mechanical Engineering; Özkan, Burcu Külahcıoğlu; Taşıran, Serdar; PhD Student; Faculty Member; Department of Mechanical Engineering; Graduate School of Sciences and Engineering; College of Engineering; N/A; N/A
    Smartphone and tablet “apps” are particularly susceptible to asynchrony bugs. In order to maintain responsive user interfaces, events are handled asynchronously. Unexpected schedules of event handlers can result in apparently-random bugs which are notoriously difficult to reproduce, even given the user-event sequences that trigger them. We develop the AsyncDroid tool for the systematic discovery and reproduction of asynchrony bugs in Android apps. Given an app and a user-event sequence, AsyncDroid systematically executes alternate schedules of the same asynchronous event handlers, according to a programmable schedule enumerator. The input user-event sequence is given either by user interaction, or can be generated by automated UI “monkeys”. By exposing and controlling the factors which influence the scheduling order of asynchronous handlers, our programmable enumerators can explicate reproducible schedules harboring bugs. By enumerating all schedules within a limited threshold of reordering, we maximize the likelihood of encountering asynchrony bugs, according to prevailing hypotheses in the literature, and discover several bugs in Android apps found in the wild.
  • Thumbnail Image
    PublicationOpen Access
    Verifying robustness of event-driven asynchronous programs against concurrency
    (Springer, 2017) Bouajjani A., Emmi M., Enea C.; Department of Computer Engineering; Özkan, Burcu Külahcıoğlu; Taşıran, Serdar; Faculty Member; Department of Computer Engineering; College of Engineering
    We define a correctness criterion, called robustness against concurrency, for a class of event-driven asynchronous programs that are at the basis of modern UI frameworks in Android, iOS, and Javascript. A program is robust when all possible behaviors admitted by the program under arbitrary procedure and event interleavings are admitted even if asynchronous procedures (respectively, events) are assumed to execute serially, one after the other, accessing shared memory in isolation. We characterize robustness as a conjunction of two correctness criteria: event-serializability (i.e., events can be seen as atomic) and event determinism (executions within each event are insensitive to the interleavings between concurrent tasks dynamically spawned by the event). Then, we provide efficient algorithms for checking these two criteria based on polynomial reductions to reachability problems in sequential programs. This result is surprising because it allows to avoid explicit handling of all concurrent executions in the analysis, which leads to an important gain in complexity. We demonstrate via case studies on Android apps that the typical mistakes programmers make are captured as robustness violations, and that violations can be detected efficiently using our approach.