GLORIA

GEOMAR Library Ocean Research Information Access

X

Your email was sent successfully. Check your inbox.

An error occurred while sending the email. Please try again.

Proceed reservation?

Export
Filter
  • Online Resource  (12)
  • Association for Computing Machinery (ACM)  (12)
Material
  • Online Resource  (12)
Publisher
  • Association for Computing Machinery (ACM)  (12)
Person/Organisation
Language
Years
  • 1
    Online Resource
    Online Resource
    Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification
    Association for Computing Machinery (ACM) ; 2023
    In:  Proceedings of the ACM on Programming Languages Vol. 7, No. POPL ( 2023-01-09), p. 2111-2140
    Details
    In: Proceedings of the ACM on Programming Languages, Association for Computing Machinery (ACM), Vol. 7, No. POPL ( 2023-01-09), p. 2111-2140
    Abstract: We present a novel approach to deciding the validity of formulas in first-order fixpoint logic with background theories and arbitrarily nested inductive and co-inductive predicates defining least and greatest fixpoints. Our approach is constraint-based, and reduces the validity checking problem of the given first-order-fixpoint logic formula (formally, an instance in a language called µCLP) to a constraint satisfaction problem for a recently introduced predicate constraint language. Coupled with an existing sound-and-relatively-complete solver for the constraint language, this novel reduction alone already gives a sound and relatively complete method for deciding µCLP validity, but we further improve it to a novel modular primal-dual method. The key observations are (1) µCLP is closed under complement such that each (co-)inductive predicate in the original primal instance has a corresponding (co-)inductive predicate representing its complement in the dual instance obtained by taking the standard De Morgan’s dual of the primal instance, and (2) partial solutions for (co-)inductive predicates synthesized during the constraint solving process of the primal side can be used as sound upper-bounds of the corresponding (co-)inductive predicates in the dual side, and vice versa. By solving the primal and dual problems in parallel and exchanging each others’ partial solutions as sound bounds, the two processes mutually reduce each others’ solution spaces, thus enabling rapid convergence. The approach is also modular in that the bounds are synthesized and exchanged at granularity of individual (co-)inductive predicates. We demonstrate the utility of our novel fixpoint logic solving by encoding a wide variety of temporal verification problems in µCLP, including termination/non-termination, LTL, CTL, and even the full modal µ-calculus model checking of infinite state programs. The encodings exploit the modularity in both the program and the property by expressing each loops and (recursive) functions in the program and sub-formulas of the property as individual (possibly nested) (co-)inductive predicates. Together with our novel modular primal-dual µCLP solving, we obtain a novel approach to efficiently solving a wide range of temporal verification problems.
    Type of Medium: Online Resource
    ISSN: 2475-1421
    URL: Article
    DOI: 10.1145/3571265
    Language: English
    Publisher: Association for Computing Machinery (ACM)
    Publication Date: 2023
    detail.hit.zdb_id: 2924207-1
    Location Call Number Limitation Availability
    BibTip Others were also interested in ...
    Online Resource
  • 2
    Online Resource
    Online Resource
    Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited Continuations
    Association for Computing Machinery (ACM) ; 2023
    In:  Proceedings of the ACM on Programming Languages Vol. 7, No. POPL ( 2023-01-09), p. 2079-2110
    Details
    In: Proceedings of the ACM on Programming Languages, Association for Computing Machinery (ACM), Vol. 7, No. POPL ( 2023-01-09), p. 2079-2110
    Abstract: Type-and-effect systems are a widely used approach to program verification, verifying the result of a computation using types, and its behavior using effects. This paper extends an effect system for verifying temporal, value-dependent properties on event sequences yielded by programs, to the delimited control operators shift0/reset0. While these delimited control operators enable useful and powerful programming techniques, they hinder reasoning about the behavior of programs because of their ability to suspend, resume, discard, and duplicate delimited continuations. This problem is more serious in effect systems for temporal properties because these systems must be capable of identifying what event sequences are yielded by captured continuations. Our key observation for achieving effective reasoning in the presence of the delimited control operators is that their use modifies answer effects, which are temporal effects of the continuations. Based on this observation, we extend an effect system for temporal verification to accommodate answer-effect modification. Allowing answer-effect modification enables easily reasoning about traces that captured continuations yield. Another novel feature of our effect system is the support for dependently typed continuations, which allows us to reason about programs more precisely. We prove soundness of the effect system for finite event sequences via type safety and that for infinite event sequences using a logical relation.
    Type of Medium: Online Resource
    ISSN: 2475-1421
    URL: Article
    DOI: 10.1145/3571264
    Language: English
    Publisher: Association for Computing Machinery (ACM)
    Publication Date: 2023
    detail.hit.zdb_id: 2924207-1
    Location Call Number Limitation Availability
    BibTip Others were also interested in ...
    Online Resource
  • 3
    Online Resource
    Online Resource
    Software model-checking as cyclic-proof search
    Association for Computing Machinery (ACM) ; 2022
    In:  Proceedings of the ACM on Programming Languages Vol. 6, No. POPL ( 2022-01-16), p. 1-29
    Details
    In: Proceedings of the ACM on Programming Languages, Association for Computing Machinery (ACM), Vol. 6, No. POPL ( 2022-01-16), p. 1-29
    Abstract: This paper shows that a variety of software model-checking algorithms can be seen as proof-search strategies for a non-standard proof system, known as a cyclic proof system . Our use of the cyclic proof system as a logical foundation of software model checking enables us to compare different algorithms, to reconstruct well-known algorithms from a few simple principles, and to obtain soundness proofs of algorithms for free. Among others, we show the significance of a heuristics based on a notion that we call maximal conservativity ; this explains the cores of important algorithms such as property-directed reachability (PDR) and reveals a surprising connection to an efficient solver of games over infinite graphs that was not regarded as a kind of PDR.
    Type of Medium: Online Resource
    ISSN: 2475-1421
    URL: Article
    DOI: 10.1145/3498725
    Language: English
    Publisher: Association for Computing Machinery (ACM)
    Publication Date: 2022
    detail.hit.zdb_id: 2924207-1
    Location Call Number Limitation Availability
    BibTip Others were also interested in ...
    Online Resource
  • 4
    Online Resource
    Online Resource
    Inductive Approach to Spacer
    Association for Computing Machinery (ACM) ; 2024
    In:  Proceedings of the ACM on Programming Languages Vol. 8, No. PLDI ( 2024-06-20), p. 1979-2002
    Details
    In: Proceedings of the ACM on Programming Languages, Association for Computing Machinery (ACM), Vol. 8, No. PLDI ( 2024-06-20), p. 1979-2002
    Abstract: The constrained Horn clause satisfiability problem is at the core of many automated verification methods, and Spacer is one of the most efficient solvers of this problem. The standard description of Spacer is based on an abstract transition system, dividing the whole procedure into small rules. This division makes individual rules easier to understand but, conversely, makes it difficult to discuss the procedure as a whole. As evidence of the difficulty in understanding the whole procedure, we point out that the claimed refutational completeness actually fails for several reasons, some of which were not present in the original version and subsequently added. It is also difficult to grasp the differences between Spacer and another procedure, such as GPDR. This paper aims to provide a better understanding of Spacer by developing a Spacer-like procedure defined by structural induction. We first formulate the problem to be solved inductively, then give its naïve solver and transform it to obtain a Spacer-like procedure. Interestingly, our inductive approach almost unifies Spacer and GPDR, which differ in only one respect in our understanding. To demonstrate the usefulness of our inductive approach in understanding Spacer, we examine Spacer variants in the literature in terms of inductive procedures and discuss why they are not refutationally complete and how to fix them. We also implemented the proposed procedure and evaluated it experimentally.
    Type of Medium: Online Resource
    ISSN: 2475-1421
    URL: Article
    DOI: 10.1145/3656457
    Language: English
    Publisher: Association for Computing Machinery (ACM)
    Publication Date: 2024
    detail.hit.zdb_id: 2924207-1
    Location Call Number Limitation Availability
    BibTip Others were also interested in ...
    Online Resource
  • 5
    Online Resource
    Online Resource
    Predicate abstraction and CEGAR for higher-order model checking
    Association for Computing Machinery (ACM) ; 2011
    In:  ACM SIGPLAN Notices Vol. 46, No. 6 ( 2011-06-04), p. 222-233
    Details
    In: ACM SIGPLAN Notices, Association for Computing Machinery (ACM), Vol. 46, No. 6 ( 2011-06-04), p. 222-233
    Abstract: Higher-order model checking (more precisely, the model checking of higher-order recursion schemes) has been extensively studied recently, which can automatically decide properties of programs written in the simply-typed λ-calculus with recursion and finite data domains. This paper formalizes predicate abstraction and counterexample-guided abstraction refinement (CEGAR) for higher-order model checking, enabling automatic verification of programs that use infinite data domains such as integers. A prototype verifier for higher-order functional programs based on the formalization has been implemented and tested for several programs.
    Type of Medium: Online Resource
    ISSN: 0362-1340 , 1558-1160
    URL: Article
    DOI: 10.1145/1993316.1993525
    Language: English
    Publisher: Association for Computing Machinery (ACM)
    Publication Date: 2011
    detail.hit.zdb_id: 282422-X
    Location Call Number Limitation Availability
    BibTip Others were also interested in ...
    Online Resource
  • 6
    Online Resource
    Online Resource
    Optimal CHC Solving via Termination Proofs
    Association for Computing Machinery (ACM) ; 2023
    In:  Proceedings of the ACM on Programming Languages Vol. 7, No. POPL ( 2023-01-09), p. 604-631
    Details
    In: Proceedings of the ACM on Programming Languages, Association for Computing Machinery (ACM), Vol. 7, No. POPL ( 2023-01-09), p. 604-631
    Abstract: Motivated by applications to open program reasoning such as maximal specification inference, this paper studies optimal CHC solving , a problem to compute maximal and/or minimal solutions of constrained Horn clauses (CHCs). This problem and its subproblems have been studied in the literature, and a major approach is to iteratively improve a solution of CHCs until it becomes optimal. So a key ingredient of optimization methods is the optimality checking of a given solution. We propose a novel optimality checking method, as well as an optimization method using the proposed optimality checker, based on a computational theoretical analysis of the optimality checking problem. The key observation is that the optimality checking problem is closely related to the termination analysis of programs, and this observation is useful both theoretically and practically. From a theoretical perspective, it clarifies a limitation of an existing method and incorrectness of another method in the literature. From a practical perspective, it allows us to apply techniques of termination analysis to the optimality checking of a solution of CHCs. We present an optimality checking method based on constraint-based synthesis of termination arguments, implemented our method, evaluated it on CHCs that encode maximal specification synthesis problems, and obtained promising results.
    Type of Medium: Online Resource
    ISSN: 2475-1421
    URL: Article
    DOI: 10.1145/3571214
    Language: English
    Publisher: Association for Computing Machinery (ACM)
    Publication Date: 2023
    detail.hit.zdb_id: 2924207-1
    Location Call Number Limitation Availability
    BibTip Others were also interested in ...
    Online Resource
  • 7
    Online Resource
    Online Resource
    Predicate abstraction and CEGAR for higher-order model checking
    Association for Computing Machinery (ACM) ; 2012
    In:  ACM SIGPLAN Notices Vol. 47, No. 6 ( 2012-08-06), p. 222-
    Details
    In: ACM SIGPLAN Notices, Association for Computing Machinery (ACM), Vol. 47, No. 6 ( 2012-08-06), p. 222-
    Type of Medium: Online Resource
    ISSN: 0362-1340
    URL: Issue
    URL: Article
    DOI: 10.1145/2345156
    DOI: 10.1145/2345156.1993525
    Language: English
    Publisher: Association for Computing Machinery (ACM)
    Publication Date: 2012
    detail.hit.zdb_id: 282422-X
    Location Call Number Limitation Availability
    BibTip Others were also interested in ...
    Online Resource
  • 8
    Online Resource
    Online Resource
    Higher-order multi-parameter tree transducers and recursion schemes for program verification
    Association for Computing Machinery (ACM) ; 2010
    In:  ACM SIGPLAN Notices Vol. 45, No. 1 ( 2010-01-02), p. 495-508
    Details
    In: ACM SIGPLAN Notices, Association for Computing Machinery (ACM), Vol. 45, No. 1 ( 2010-01-02), p. 495-508
    Abstract: We introduce higher-order, multi-parameter, tree transducers (HMTTs, for short), which are kinds of higher-order tree transducers that take input trees and output a (possibly infinite) tree. We study the problem of checking whether the tree generated by a given HMTT conforms to a given output specification, provided that the input trees conform to input specifications (where both input/output specifications are regular tree languages). HMTTs subsume higher-order recursion schemes and ordinary tree transducers, so that their verification has a number of potential applications to verification of functional programs using recursive data structures, including resource usage verification, string analysis, and exact type-checking of XML-processing programs. We propose a sound but incomplete verification algorithm for the HMTT verification problem: the algorithm reduces the verification problem to a model-checking problem for higher-order recursion schemes extended with finite data domains, and then uses (an extension of)Kobayashi's algorithm for model-checking recursion schemes. While the algorithm is incomplete (indeed, as we show in the paper, the verification problem is undecidable in general), it is sound and complete for a subclass of HMTTs called linear HMTTs . We have applied our HMTT verification algorithm to various program verification problems and obtained promising results.
    Type of Medium: Online Resource
    ISSN: 0362-1340 , 1558-1160
    URL: Article
    DOI: 10.1145/1707801.1706355
    Language: English
    Publisher: Association for Computing Machinery (ACM)
    Publication Date: 2010
    detail.hit.zdb_id: 282422-X
    Location Call Number Limitation Availability
    BibTip Others were also interested in ...
    Online Resource
  • 9
    Online Resource
    Online Resource
    Temporal verification of higher-order functional programs
    Association for Computing Machinery (ACM) ; 2016
    In:  ACM SIGPLAN Notices Vol. 51, No. 1 ( 2016-04-08), p. 57-68
    Details
    In: ACM SIGPLAN Notices, Association for Computing Machinery (ACM), Vol. 51, No. 1 ( 2016-04-08), p. 57-68
    Abstract: We present an automated approach to verifying arbitrary omega-regular properties of higher-order functional programs. Previous automated methods proposed for this class of programs could only handle safety properties or termination, and our approach is the first to be able to verify arbitrary omega-regular liveness properties. Our approach is automata-theoretic, and extends our recent work on binary-reachability-based approach to automated termination verification of higher-order functional programs to fair termination published in ESOP 2014. In that work, we have shown that checking disjunctive well-foundedness of (the transitive closure of) the ``calling relation'' is sound and complete for termination. The extension to fair termination is tricky, however, because the straightforward extension that checks disjunctive well-foundedness of the fair calling relation turns out to be unsound, as we shall show in the paper. Roughly, our solution is to check fairness on the transition relation instead of the calling relation, and propagate the information to determine when it is necessary and sufficient to check for disjunctive well-foundedness on the calling relation. We prove that our approach is sound and complete. We have implemented a prototype of our approach, and confirmed that it is able to automatically verify liveness properties of some non-trivial higher-order programs.
    Type of Medium: Online Resource
    ISSN: 0362-1340 , 1558-1160
    URL: Article
    DOI: 10.1145/2914770.2837667
    Language: English
    Publisher: Association for Computing Machinery (ACM)
    Publication Date: 2016
    detail.hit.zdb_id: 282422-X
    Location Call Number Limitation Availability
    BibTip Others were also interested in ...
    Online Resource
  • 10
    Online Resource
    Online Resource
    Automating relatively complete verification of higher-order functional programs
    Association for Computing Machinery (ACM) ; 2013
    In:  ACM SIGPLAN Notices Vol. 48, No. 1 ( 2013-01-23), p. 75-86
    Details
    In: ACM SIGPLAN Notices, Association for Computing Machinery (ACM), Vol. 48, No. 1 ( 2013-01-23), p. 75-86
    Abstract: We present an automated approach to relatively completely verifying safety (i.e., reachability) property of higher-order functional programs. Our contribution is two-fold. First, we extend the refinement type system framework employed in the recent work on (incomplete) automated higher-order verification by drawing on the classical work on relatively complete "Hoare logic like" program logic for higher-order procedural languages. Then, by adopting the recently proposed techniques for solving constraints over quantified first-order logic formulas, we develop an automated type inference method for the type system, thereby realizing an automated relatively complete verification of higher-order programs.
    Type of Medium: Online Resource
    ISSN: 0362-1340 , 1558-1160
    URL: Article
    DOI: 10.1145/2480359.2429081
    Language: English
    Publisher: Association for Computing Machinery (ACM)
    Publication Date: 2013
    detail.hit.zdb_id: 282422-X
    Location Call Number Limitation Availability
    BibTip Others were also interested in ...
    Online Resource
Close ⊗
This website uses cookies and the analysis tool Matomo. More information can be found here...