Journal: Formal Methods in System Design

Abbreviation

Form Methods Syst Des

Publisher

Springer

Journal Volumes

ISSN

0925-9856
1572-8102

Description

Filters

Reset filters

Search Results

Publications 1 - 10 of 11
  • A survey of challenges for runtime verification from advanced application domains (beyond software)
    Item type: Journal Article
    Sánchez, César; Schneider, Gerardo; Ahrendt, Wolfgang; et al. (2019)
    Formal Methods in System Design
    Runtime verification is an area of formal methods that studies the dynamic analysis of execution traces against formal specifications. Typically, the two main activities in runtime verification efforts are the process of creating monitors from specifications, and the algorithms for the evaluation of traces against the generated monitors. Other activities involve the instrumentation of the system to generate the trace and the communication between the system under analysis and the monitor. Most of the applications in runtime verification have been focused on the dynamic analysis of software, even though there are many more potential applications to other computational devices and target systems. In this paper we present a collection of challenges for runtime verification extracted from concrete application domains, focusing on the difficulties that must be overcome to tackle these specific challenges. The computational models that characterize these domains require to devise new techniques beyond the current state of the art in runtime verification.
  • Verification of SpecC using predicate abstraction
    Item type: Journal Article
    Clarke, Edmund; Jain, Himanshu; Kroening, Daniel (2007)
    Formal Methods in System Design
  • Predicate Abstraction of ANSI-C Programs Using SAT
    Item type: Journal Article
    Clarke, Edmund; Kroening, Daniel; Sharygina, Natasha; et al. (2004)
    Formal Methods in System Design
  • Partially-shared zero-suppressed multi-terminal BDDs
    Item type: Journal Article
    Lampka, Kai; Siegle, Markus; Ossowski, Joern; et al. (2010)
    Formal Methods in System Design
  • Efficient data race detection for async-finish parallelism
    Item type: Journal Article
    Raman, Raghavan; Zhao, Jisheng; Sarkar, Vivek; et al. (2012)
    Formal Methods in System Design
  • Don’t care words with an application to the automata-based approach for real addition
    Item type: Journal Article
    Eisinger, Jochen; Klaedtke, Felix (2008)
    Formal Methods in System Design
  • Context-aware counter abstraction
    Item type: Journal Article
    Basler, Gérard; Mazzucchi, Michele; Wahl, Thomas; et al. (2010)
    Formal Methods in System Design
  • Monitoring of Temporal First-order Properties with Aggregations
    Item type: Journal Article
    Basin, David; Klaedtke, Felix; Marinovic, Srdjan; et al. (2015)
    Formal Methods in System Design
    In system monitoring, one is often interested in checking properties of aggregated data. Current policy monitoring approaches are limited in the kinds of aggregations they handle. To rectify this, we extend an expressive language, metric first-order temporal logic, with aggregation operators. Our extension is inspired by the aggregation operators common in database query languages like SQL. We provide a monitoring algorithm for this enriched policy specification language. We show that, in comparison to related data processing approaches, our language is better suited for expressing policies, and our monitoring algorithm has competitive performance.
  • Almost event-rate independent monitoring
    Item type: Journal Article
    Basin, David; Bhatt, Bhargav N.; Krstić, Srđan; et al. (2019)
    Formal Methods in System Design
    A monitoring algorithm is trace-length independent if its space consumption does not depend on the number of events processed. The analysis of many monitoring algorithms has aimed at establishing their trace-length independence. But a monitor’s space consumption can depend on characteristics of the trace other than its size. We put forward the stronger notion of event-rate independence, where a monitor’s space usage does not depend on the event rate, i.e., the number of events in a fixed time unit. This property is critical for monitoring voluminous streams of events with a high arrival rate. We propose a new algorithm for metric temporal logic (MTL) that is almost event-rate independent, where “almost” denotes a logarithmic dependence on the event rate: the algorithm must store the event rate as a number. Afterwards, we investigate more expressive logics. In particular, we extend linear dynamic logic with past operators and metric features. The resulting metric dynamic logic (MDL) offers the quantitative temporal conveniences of MTL while increasing its expressiveness. We show how to modify our MTL algorithm in a modular way, yielding an almost event-rate independent monitor for MDL. Finally, we compare our algorithms with traditional monitoring approaches, providing empirical evidence that almost event-rate independence matters in practice.
  • Concise outlines for a complex logic: a proof outline checker for TaDA
    Item type: Journal Article
    Wolf, Felix; Schwerhoff, Malte; Müller, Peter (2023)
    Formal Methods in System Design
    Modern separation logics allow one to prove rich properties of intricate code, e.g., functional correctness and linearizability of non-blocking concurrent code. However, this expressiveness leads to a complexity that makes these logics difficult to apply. Manual proofs or proofs in interactive theorem provers consist of a large number of steps, often with subtle side conditions. On the other hand, automation with dedicated verifiers typically requires sophisticated proof search algorithms that are specific to the given program logic, resulting in limited tool support that makes it difficult to experiment with program logics, e.g., when learning, improving, or comparing them. Proof outline checkers fill this gap. Their input is a program annotated with the most essential proof steps, just like the proof outlines typically presented in papers. The tool then checks automatically that this outline represents a valid proof in the program logic. In this paper, we systematically develop a proof outline checker for the TaDA logic, which reduces the checking to a simpler verification problem, for which automated tools exist. Our approach leads to proof outline checkers that provide substantially more automation than interactive provers, but are much simpler to develop than custom automatic verifiers.
Publications 1 - 10 of 11