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
  • Association for Computing Machinery (ACM)  (35)
  • 1
    Online Resource
    Online Resource
    Verifying security invariants in ExpressOS
    Association for Computing Machinery (ACM) ; 2013
    In:  ACM SIGARCH Computer Architecture News Vol. 41, No. 1 ( 2013-03-29), p. 293-304
    Details
    In: ACM SIGARCH Computer Architecture News, Association for Computing Machinery (ACM), Vol. 41, No. 1 ( 2013-03-29), p. 293-304
    Abstract: Security for applications running on mobile devices is important. In this paper we present ExpressOS, a new OS for enabling high-assurance applications to run on commodity mobile devices securely. Our main contributions are a new OS architecture and our use of formal methods for proving key security invariants about our implementation. In our use of formal methods, we focus solely on proving that our OS implements our security invariants correctly, rather than striving for full functional correctness, requiring significantly less verification effort while still proving the security relevant aspects of our system. We built ExpressOS, analyzed its security, and tested its performance. Our evaluation shows that the performance of ExpressOS is comparable to an Android-based system. In one test, we ran the same web browser on ExpressOS and on an Android-based system, and found that ExpressOS adds 16% overhead on average to the page load latency time for nine popular web sites.
    Type of Medium: Online Resource
    ISSN: 0163-5964
    URL: Article
    DOI: 10.1145/2490301.2451148
    RVK:
    SS 1985
    Language: English
    Publisher: Association for Computing Machinery (ACM)
    Publication Date: 2013
    detail.hit.zdb_id: 2088489-8
    detail.hit.zdb_id: 186012-4
    Location Call Number Limitation Availability
    BibTip Others were also interested in ...
    Online Resource
  • 2
    Online Resource
    Online Resource
    Learning formulas in finite variable logics
    Association for Computing Machinery (ACM) ; 2022
    In:  Proceedings of the ACM on Programming Languages Vol. 6, No. POPL ( 2022-01-16), p. 1-28
    Details
    In: Proceedings of the ACM on Programming Languages, Association for Computing Machinery (ACM), Vol. 6, No. POPL ( 2022-01-16), p. 1-28
    Abstract: We consider grammar-restricted exact learning of formulas and terms in finite variable logics. We propose a novel and versatile automata-theoretic technique for solving such problems. We first show results for learning formulas that classify a set of positively- and negatively-labeled structures. We give algorithms for realizability and synthesis of such formulas along with upper and lower bounds. We also establish positive results using our technique for other logics and variants of the learning problem, including first-order logic with least fixed point definitions, higher-order logics, and synthesis of queries and terms with recursively-defined functions.
    Type of Medium: Online Resource
    ISSN: 2475-1421
    URL: Article
    DOI: 10.1145/3498671
    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
  • 3
    Online Resource
    Online Resource
    Adding nesting structure to words
    Association for Computing Machinery (ACM) ; 2009
    In:  Journal of the ACM Vol. 56, No. 3 ( 2009-05), p. 1-43
    Details
    In: Journal of the ACM, Association for Computing Machinery (ACM), Vol. 56, No. 3 ( 2009-05), p. 1-43
    Abstract: We propose the model of nested words for representation of data with both a linear ordering and a hierarchically nested matching of items. Examples of data with such dual linear-hierarchical structure include executions of structured programs, annotated linguistic data, and HTML/XML documents. Nested words generalize both words and ordered trees, and allow both word and tree operations. We define nested word automata —finite-state acceptors for nested words, and show that the resulting class of regular languages of nested words has all the appealing theoretical properties that the classical regular word languages enjoys: deterministic nested word automata are as expressive as their nondeterministic counterparts; the class is closed under union, intersection, complementation, concatenation, Kleene-*, prefixes, and language homomorphisms; membership, emptiness, language inclusion, and language equivalence are all decidable; and definability in monadic second order logic corresponds exactly to finite-state recognizability. We also consider regular languages of infinite nested words and show that the closure properties, MSO-characterization, and decidability of decision problems carry over. The linear encodings of nested words give the class of visibly pushdown languages of words, and this class lies between balanced languages and deterministic context-free languages. We argue that for algorithmic verification of structured programs, instead of viewing the program as a context-free language over words, one should view it as a regular language of nested words (or equivalently, a visibly pushdown language), and this would allow model checking of many properties (such as stack inspection, pre-post conditions) that are not expressible in existing specification logics. We also study the relationship between ordered trees and nested words, and the corresponding automata: while the analysis complexity of nested word automata is the same as that of classical tree automata, they combine both bottom-up and top-down traversals, and enjoy expressiveness and succinctness benefits over tree automata.
    Type of Medium: Online Resource
    ISSN: 0004-5411 , 1557-735X
    URL: Article
    DOI: 10.1145/1516512.1516518
    RVK:
    SA 3010
    Language: English
    Publisher: Association for Computing Machinery (ACM)
    Publication Date: 2009
    detail.hit.zdb_id: 2006500-0
    detail.hit.zdb_id: 6759-3
    Location Call Number Limitation Availability
    BibTip Others were also interested in ...
    Online Resource
  • 4
    Online Resource
    Online Resource
    Synthesis of interface specifications for Java classes
    Association for Computing Machinery (ACM) ; 2005
    In:  ACM SIGPLAN Notices Vol. 40, No. 1 ( 2005-01-12), p. 98-109
    Details
    In: ACM SIGPLAN Notices, Association for Computing Machinery (ACM), Vol. 40, No. 1 ( 2005-01-12), p. 98-109
    Abstract: While a typical software component has a clearly specified (static) interface in terms of the methods and the input/output types they support, information about the correct sequencing of method calls the client must invoke is usually undocumented. In this paper, we propose a novel solution for automatically extracting such temporal specifications for Java classes. Given a Java class, and a safety property such as "the exception E should not be raised", the corresponding (dynamic) interface is the most general way of invoking the methods in the class so that the safety property is not violated. Our synthesis method first constructs a symbolic representation of the finite state-transition system obtained from the class using predicate abstraction . Constructing the interface then corresponds to solving a partial-information two-player game on this symbolic graph. We present a sound approach to solve this computationally-hard problem approximately using algorithms for learning finite automata and symbolic model checking for branching-time logics. We describe an implementation of the proposed techniques in the tool JIST --- Java Interface Synthesis Tool---and demonstrate that the tool can construct interfaces accurately and efficiently for sample Java2SDK library classes.
    Type of Medium: Online Resource
    ISSN: 0362-1340 , 1558-1160
    URL: Article
    DOI: 10.1145/1047659.1040314
    Language: English
    Publisher: Association for Computing Machinery (ACM)
    Publication Date: 2005
    detail.hit.zdb_id: 2079194-X
    detail.hit.zdb_id: 282422-X
    Location Call Number Limitation Availability
    BibTip Others were also interested in ...
    Online Resource
  • 5
    Online Resource
    Online Resource
    Esports and expertise : what competitive gaming can teach us about mastery
    Association for Computing Machinery (ACM) ; 2022
    In:  Interactions Vol. 29, No. 6 ( 2022-11), p. 54-59
    Details
    In: Interactions, Association for Computing Machinery (ACM), Vol. 29, No. 6 ( 2022-11), p. 54-59
    Type of Medium: Online Resource
    ISSN: 1072-5520 , 1558-3449
    URL: Article
    DOI: 10.1145/3567954
    Language: English
    Publisher: Association for Computing Machinery (ACM)
    Publication Date: 2022
    detail.hit.zdb_id: 2002363-7
    detail.hit.zdb_id: 1214813-1
    SSG: 24
    Location Call Number Limitation Availability
    BibTip Others were also interested in ...
    Online Resource
  • 6
    Online Resource
    Online Resource
    Compositional Synthesis of Piece-Wise Functions by Learning Classifiers
    Association for Computing Machinery (ACM) ; 2018
    In:  ACM Transactions on Computational Logic Vol. 19, No. 2 ( 2018-04-30), p. 1-23
    Details
    In: ACM Transactions on Computational Logic, Association for Computing Machinery (ACM), Vol. 19, No. 2 ( 2018-04-30), p. 1-23
    Abstract: We present a novel general technique that uses classifier learning to synthesize piece-wise functions (functions that split the domain into regions and apply simpler functions to each region) against logical synthesis specifications. Our framework works by combining a synthesizer of functions for fixed concrete inputs and a synthesizer of predicates that can be used to define regions. We develop a theory of single-point refutable specifications that facilitate generating concrete counterexamples using constraint solvers. We implement the framework for synthesizing piece-wise functions in linear integer arithmetic, combining leaf expression synthesis using constraint-solving with predicate synthesis using enumeration, and tie them together using a decision tree classifier. We demonstrate that this compositional approach is competitive compared to existing synthesis engines on a set of synthesis specifications.
    Type of Medium: Online Resource
    ISSN: 1529-3785 , 1557-945X
    URL: Article
    DOI: 10.1145/3173545
    Language: English
    Publisher: Association for Computing Machinery (ACM)
    Publication Date: 2018
    detail.hit.zdb_id: 2025647-4
    Location Call Number Limitation Availability
    BibTip Others were also interested in ...
    Online Resource
  • 7
    Online Resource
    Online Resource
    Natural proofs for data structure manipulation in C using separation logic
    Association for Computing Machinery (ACM) ; 2014
    In:  ACM SIGPLAN Notices Vol. 49, No. 6 ( 2014-06-05), p. 440-451
    Details
    In: ACM SIGPLAN Notices, Association for Computing Machinery (ACM), Vol. 49, No. 6 ( 2014-06-05), p. 440-451
    Abstract: The natural proof technique for heap verification developed by Qiu et al. [32] provides a platform for powerful sound reasoning for specifications written in a dialect of separation logic called Dryad. Natural proofs are proof tactics that enable automated reasoning exploiting recursion, mimicking common patterns found in human proofs. However, these proofs are known to work only for a simple toy language [32] . In this work, we develop a framework called VCDryad that extends the Vcc framework [9] to provide an automated deductive framework against separation logic specifications for C programs based on natural proofs. We develop several new techniques to build this framework, including (a) a novel tool architecture that allows encoding natural proofs at a higher level in order to use the existing Vcc framework (including its intricate memory model, the underlying type-checker, and the SMT-based verification infrastructure), and (b) a synthesis of ghost-code annotations that captures natural proof tactics, in essence forcing Vcc to find natural proofs using primarily decidable theories. We evaluate our tool extensively, on more than 150 programs, ranging from code manipulating standard data structures, well-known open source library routines (Glib, OpenBSD), Linux kernel routines, customized OS data structures, etc. We show that all these C programs can be fully automatically verified using natural proofs (given pre/post conditions and loop invariants) without any user-provided proof tactics . VCDryad is perhaps the first deductive verification framework for heap-manipulating programs in a real language that can prove such a wide variety of programs automatically.
    Type of Medium: Online Resource
    ISSN: 0362-1340 , 1558-1160
    URL: Article
    DOI: 10.1145/2666356.2594325
    Language: English
    Publisher: Association for Computing Machinery (ACM)
    Publication Date: 2014
    detail.hit.zdb_id: 2079194-X
    detail.hit.zdb_id: 282422-X
    Location Call Number Limitation Availability
    BibTip Others were also interested in ...
    Online Resource
  • 8
    Online Resource
    Online Resource
    Session details: Verification 2
    Association for Computing Machinery (ACM) ; 2014
    In:  ACM SIGPLAN Notices Vol. 49, No. 6 ( 2014-06-05)
    Details
    In: ACM SIGPLAN Notices, Association for Computing Machinery (ACM), Vol. 49, No. 6 ( 2014-06-05)
    Type of Medium: Online Resource
    ISSN: 0362-1340 , 1558-1160
    URL: Article
    DOI: 10.1145/3263313
    Language: English
    Publisher: Association for Computing Machinery (ACM)
    Publication Date: 2014
    detail.hit.zdb_id: 2079194-X
    detail.hit.zdb_id: 282422-X
    Location Call Number Limitation Availability
    BibTip Others were also interested in ...
    Online Resource
  • 9
    Online Resource
    Online Resource
    Session details: 3.B: complexity for concurrency
    Association for Computing Machinery (ACM) ; 2012
    In:  ACM SIGPLAN Notices Vol. 47, No. 1 ( 2012-01-18)
    Details
    In: ACM SIGPLAN Notices, Association for Computing Machinery (ACM), Vol. 47, No. 1 ( 2012-01-18)
    Type of Medium: Online Resource
    ISSN: 0362-1340 , 1558-1160
    URL: Article
    DOI: 10.1145/3261830
    Language: English
    Publisher: Association for Computing Machinery (ACM)
    Publication Date: 2012
    detail.hit.zdb_id: 2079194-X
    detail.hit.zdb_id: 282422-X
    Location Call Number Limitation Availability
    BibTip Others were also interested in ...
    Online Resource
  • 10
    Online Resource
    Online Resource
    Learning invariants using decision trees and implication counterexamples
    Association for Computing Machinery (ACM) ; 2016
    In:  ACM SIGPLAN Notices Vol. 51, No. 1 ( 2016-04-08), p. 499-512
    Details
    In: ACM SIGPLAN Notices, Association for Computing Machinery (ACM), Vol. 51, No. 1 ( 2016-04-08), p. 499-512
    Abstract: Inductive invariants can be robustly synthesized using a learning model where the teacher is a program verifier who instructs the learner through concrete program configurations, classified as positive, negative, and implications. We propose the first learning algorithms in this model with implication counter-examples that are based on machine learning techniques. In particular, we extend classical decision-tree learning algorithms in machine learning to handle implication samples, building new scalable ways to construct small decision trees using statistical measures. We also develop a decision-tree learning algorithm in this model that is guaranteed to converge to the right concept (invariant) if one exists. We implement the learners and an appropriate teacher, and show that the resulting invariant synthesis is efficient and convergent for a large suite of programs.
    Type of Medium: Online Resource
    ISSN: 0362-1340 , 1558-1160
    URL: Article
    DOI: 10.1145/2914770.2837664
    Language: English
    Publisher: Association for Computing Machinery (ACM)
    Publication Date: 2016
    detail.hit.zdb_id: 2079194-X
    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...