The Experts below are selected from a list of 360 Experts worldwide ranked by ideXlab platform

Byron Cook - One of the best experts on this subject based on the ideXlab platform.

  • Formal Reasoning about the security of amazon web services
    Computer Aided Verification, 2018
    Co-Authors: Byron Cook
    Abstract:

    We report on the development and use of Formal verification tools within Amazon Web Services (AWS) to increase the security assurance of its cloud infrastructure and to help customers secure themselves. We also discuss some remaining challenges that could inspire future research in the community.

  • automated Formal Reasoning about amazon web services keynote
    Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software, 2017
    Co-Authors: Byron Cook
    Abstract:

    Automatic and semiautomatic Formal verification and model checking tools are now being used within AWS to find proofs that prove or disprove desired properties of key AWS components. In this session, we outline these efforts and discuss how tools are used to play and then replay found proofs of desired properties when software artifacts or networks are modified, thus helping provide security throughout the lifetime of the AWS system.

  • Automated Formal Reasoning about AWS systems
    2017 Formal Methods in Computer Aided Design (FMCAD), 2017
    Co-Authors: Byron Cook
    Abstract:

    Automatic and semiautomatic Formal verification tools are now being developed and used within Amazon Web Services (AWS) to find proofs that prove or disprove desired properties of key AWS components. In this session, we outline these efforts and discuss how tools are used to play and then replay found proofs of desired properties when software artifacts or networks are modified, thus helping provide security throughout the lifetime of the AWS system.

Manny Rayner - One of the best experts on this subject based on the ideXlab platform.

  • on the applicability of nonmonotonic logic to Formal Reasoning in continuous time
    Artificial Intelligence, 1991
    Co-Authors: Manny Rayner
    Abstract:

    The paper criticizes arguments recently advanced by Shoham, McDermott and Sandewall, which purport to demonstrate the relevance of non-monotonic logic to the Formalization of Reasoning about the evolution of mechanical systems in continuous time. The first half of the paper examines the "Extended Prediction Problem" of Shoham and McDermott; reasons are given to support the claim that the "problem" is the product of a mistaken understanding of the the Formal basis of Newtonian mechanics, and has no real existence. An example is given showing how, contrary to Shoham and McDermott's arguments, it is possible to Formalise Reasoning about the evolution of physical systems in continuous time using only classical logic and differential calculus. The second half then reviews Sandewall's non-monotonic logic for almost-continuous systems. Here it is argued that the proposed framework offers only very marginal advantages in compactness of notation, and generally tends to collapse back into classical logic. In summary, I conclude that there is as yet no good reason to believe that non-monotonic logic will be a useful tool in this area.

  • on the applicability of nonmonotonic logic to Formal Reasoning in continuous time
    Artificial Intelligence, 1991
    Co-Authors: Manny Rayner
    Abstract:

    The paper criticizes arguments recently advanced by Shoham, McDermott and Sandewall, which purport to demonstrate the relevance of non-monotonic logic to the Formalization of Reasoning about the evolution of mechanical systems in continuous time. The first half of the paper examines the "Extended Prediction Problem" of Shoham and McDermott; reasons are given to support the claim that the "problem" is the product of a mistaken understanding of the the Formal basis of Newtonian mechanics, and has no real existence. An example is given showing how, contrary to Shoham and McDermott's arguments, it is possible to Formalise Reasoning about the evolution of physical systems in continuous time using only classical logic and differential calculus. The second half then reviews Sandewall's non-monotonic logic for almost-continuous systems. Here it is argued that the proposed framework offers only very marginal advantages in compactness of notation, and generally tends to collapse back into classical logic. In summary, I conclude that there is as yet no good reason to believe that non-monotonic logic will be a useful tool in this area.

Bartek Klin - One of the best experts on this subject based on the ideXlab platform.

  • bialgebraic methods and modal logic in structural operational semantics
    Information & Computation, 2009
    Co-Authors: Bartek Klin
    Abstract:

    Bialgebraic semantics, invented a decade ago by Turi and Plotkin, is an approach to Formal Reasoning about well-behaved structural operational semantics (SOS). An extension of algebraic and coalgebraic methods, it abstracts from concrete notions of syntax and system behaviour, thus treating various kinds of operational descriptions in a uniform fashion. In this paper, bialgebraic semantics is combined with a coalgebraic approach to modal logic in a novel, general approach to proving the compositionality of process equivalences for languages defined by structural operational semantics. To prove compositionality, one provides a notion of behaviour for logical formulas, and defines an SOS-like specification of modal operators which reflects the original SOS specification of the language. This approach can be used to define SOS congruence formats as well as to prove compositionality for specific languages and equivalences.

Thorsten Altenkirch - One of the best experts on this subject based on the ideXlab platform.

  • a Formalization of the strong normalization proof for system f in lego
    International Conference on Typed Lambda Calculi and Applications, 1993
    Co-Authors: Thorsten Altenkirch
    Abstract:

    We describe a complete Formalization of a strong normalization proof for the Curry style presentation of System F in LEGO. The underlying type theory is the Calculus of Constructions enriched by inductive types. The proof follows Girard et al [GLT89], i.e. we use the notion of candidates of reducibility, but we make essential use of general inductive types to simplify the presentation. We discuss extensions and variations of the proof: the extraction of a normalization function, the use of saturated sets instead of candidates, and the extension to a Church Style presentation. We conclude with some general observations about Computer Aided Formal Reasoning.

  • a Formalization of the strong normalization proof for system f in lego
    International Conference on Typed Lambda Calculi and Applications, 1993
    Co-Authors: Thorsten Altenkirch
    Abstract:

    We describe a complete Formalization of a strong normalization proof for the Curry style presentation of System F in LEGO. The underlying type theory is the Calculus of Constructions enriched by inductive types. The proof follows Girard et al [GLT89], i.e. we use the notion of candidates of reducibility, but we make essential use of general inductive types to simplify the presentation. We discuss extensions and variations of the proof: the extraction of a normalization function, the use of saturated sets instead of candidates, and the extension to a Church Style presentation. We conclude with some general observations about Computer Aided Formal Reasoning.

Abhik Roychoudhury - One of the best experts on this subject based on the ideXlab platform.

  • Formal Reasoning about hardware and software memory models
    International Conference on Formal Engineering Methods, 2002
    Co-Authors: Abhik Roychoudhury
    Abstract:

    The Java programming language allows multithreaded programming, where threads can be run on multiprocessor or uniprocessor platforms. The allowed behaviors of any multithreaded Java program on any implementation platform (multi- or uni-processor), are described in terms of a memory consistency model called the Java Memory Model (JMM). However, shared memory multiprocessors have a memory model of their own. To reason about the behavior of multithreaded Java programs on multiprocessors, we need a Formal basis for understanding both the hardware memory model (of the multiprocessor platform) and the software memory model (the JMM). For this purpose, we have implemented Formal executable specifications of the JMM and certain hardware memory models (such as TSO/PSO from SPARC). These executable specifications can be used for exhaustive search i.e. computing all allowed behaviors of test programs under the JMM and the hardware memory models. Consequently, we can compare the JMM with the hardware memory models (in terms of allowed behaviors). We show that such a comparison can help efficient and reliable multithreaded programming on multiprocessors. Results from comparing the current JMM with SPARC architecture memory models are presented.