Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userAn extended and more practical mwp flow analysis
200
0
0.0
(
0
)
Added by
Clement Aubert
Publication date
2021
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
We improve and refine a method for certifying that the values sizes computed by an imperative program will be bounded by polynomials in the programs inputs sizes. Our work tames the non-determinism of the original analysis, and offers an innovative way of completing the analysis when a non-polynomial growth is found. We furthermore enrich the analyzed language by adding function definitions and calls, allowing to compose the analysis of different libraries and offering generally more modularity. The implementation of our improved method, discussed in a tool paper (https://hal.archives-ouvertes.fr/hal-03269121), also required to reason about the efficiency of some of the needed operations on the matrices produced by the analysis. It is our hope that this work will enable and facilitate static analysis of source code to guarantee its correctness with respect to resource usages.
rate research
Read More
This volume contains a selection of papers presented at Linearity/TLLA 2018: Joint Linearity and TLLA workshops (part of FLOC 2018) held on July 7-8, 2018 in Oxford. Linearity has been a key feature in several lines of research in both theoretical and practical approaches to computer science. On the theoretical side there is much work stemming from linear logic dealing with proof technology, complexity classes and more recently quantum computation. On the practical side there is work on program analysis, expressive operational semantics for programming languages, linear programming languages, program transformation, update analysis and efficient implementation techniques. Linear logic is not only a theoretical tool to analyse the use of resources in logic and computation. It is also a corpus of tools, approaches, and methodologies (proof nets, exponential decomposition, geometry of interaction, coherent spaces, relational models, etc.) that were originally developed for the study of linear logics syntax and semantics and are nowadays applied in several other fields.
We study counting propositional logic as an extension of propositional logic with counting quantifiers. We prove that the complexity of the underlying decision problem perfectly matches the appropriate level of Wagners counting hierarchy, but also that the resulting logic admits a satisfactory proof-theoretical treatment. From the latter, a type system for a probabilistic lambda-calculus is derived in the spirit of the Curry-Howard correspondence, showing the potential of counting propositional logic as a useful tool in several fields of theoretical computer science.
This is an extended abstract presenting new results on the topological complexity of omega-powers (which are included in a paper Classical and effective descriptive complexities of omega-powers available from arXiv:0708.4176) and reflecting also some open questions which were discussed during the Dagstuhl seminar on Topological and Game-Theoretic Aspects of Infinite Computations 29.06.08 - 04.07.08.
It is common to prove by reasoning over source code that programs do not leak sensitive data. But doing so leaves a gap between reasoning and reality that can only be filled by accounting for the behaviour of the compiler. This task is complicated when programs enforce value-dependent information-flow security properties (in which classification of locations can vary depending on values in other locations) and complicated further when programs exploit shared-variable concurrency. Prior work has formally defined a notion of concurrency-aware refinement for preserving value-dependent security properties. However, that notion is considerably more complex than standard refinement definitions typically applied in the verification of semantics preservation by compilers. To date it remains unclear whether it can be applied to a realistic compiler, because there exist no general decomposition principles for separating it into smaller, more familiar, proof obligations. In this work, we provide such a decomposition principle, which we show can almost halve the complexity of proving secure refinement. Further, we demonstrate its applicability to secure compilation, by proving in Isabelle/HOL the preservation of value-dependent security by a proof-of-concept compiler from an imperative While language to a generic RISC-style assembly language, for programs with shared-memory concurrency mediated by locking primitives. Finally, we execute our compiler in Isabelle on a While language model of the Cross Domain Desktop Compositor, demonstrating to our knowledge the first use of a compiler verification result to carry an information-flow security property down to the assembly-level model of a non-trivial concurrent program.
A key component of mathematical reasoning is the ability to formulate interesting conjectures about a problem domain at hand. In this paper, we give a brief overview of a theory exploration system called QuickSpec, which is able to automatically discover interesting conjectures about a given set of functions. QuickSpec works by interleaving term generation with random testing to form candidate conjectures. This is made tractable by starting from small sizes and ensuring that only terms that are irreducible with respect to already discovered conjectures are considered. QuickSpec has been successfully applied to generate lemmas for automated inductive theorem proving as well as to generate specifications of functional programs. We give an overview of typical use-cases of QuickSpec, as well as demonstrating how to easily connect it to a theorem prover of the users choice.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
