We develop a static deadlock analysis for commercial Android Java applications, of sizes in the tens of millions of LoC, under active development at Facebook. The analysis runs primarily at code-review time, on only the modified code and its dependents; we aim at reporting to developers in under 15 minutes.To detect deadlocks in this setting, we first model the real language as an abstract language with balanced re-entrant locks, nondeterministic iteration and branching, and non-recursive procedure calls. We show that the existence of a deadlock in this abstract language is equivalent to a certain condition over the sets of critical pairs of each program thread; these record, for all possible executions of the thread, which locks are currently held at the point when a fresh lock is acquired. Since the critical pairs of any program thread is finite and computable, the deadlock detection problem for our language is decidable, and in NP.We then leverage these results to develop an open-source implementation of our analysis adapted to deal with real Java code. The core of the implementation is an algorithm which computes critical pairs in a compositional, abstract interpretation style, running in quasi-exponential time. Our analyser is built in the Infer verification framework and has been in industrial deployment for over two years; it has seen over two hundred fixed deadlock reports with a report fix rate of ~54%.

SL-COMP aims at bringing together researchers interested on improving the state of the art of the automated deduction methods for Separation Logic (SL). The event took place twice until now and collected more than 1K problems for different fragments of SL. The input format of problems is based on the SMT-LIB format and therefore fully typed; only one new command is added to SMT-LIB’s list, the command for the declaration of the heap’s type. The SMT-LIB theory of SL comes with ten logics, some of them being combinations of SL with linear arithmetics. The competition’s divisions are defined by the logic fragment, the kind of decision problem (satisfiability or entailment) and the presence of quantifiers. Until now, SL-COMP has been run on the StarExec platform, where the benchmark set and the binaries of participant solvers are freely available. The benchmark set is also available with the competition’s documentation on a public repository in GitHub.

RacerD is a static race detector that has been proven to be effective in engineering practice: it has seen thousands of data races fixed by developers before reaching production, and has supported the migration of Facebook's Android app rendering infrastructure from a single-threaded to a multi-threaded architecture. We prove a True Positives Theorem stating that, under certain assumptions, an idealized theoretical version of the analysis never reports a false positive. We also provide an empirical evaluation of an implementation of this analysis, versus the original RacerD. The theorem was motivated in the first case by the desire to understand the observation from production that RacerD was providing remarkably accurate signal to developers, and then the theorem guided further analyzer design decisions. Technically, our result can be seen as saying that the analysis computes an under-approximation of an over-approximation, which is the reverse of the more usual (over of under) situation in static analysis. Until now, static analyzers that are effective in practice but unsound have often been regarded as ad hoc; in contrast, we suggest that, in the future, theorems of this variety might be generally useful in understanding, justifying and designing effective static analyses for bug catching.

Automatic static detection of data races is one of the most basic problems in reasoning about concurrency. We present RacerD—a static program analysis for detecting data races in Java programs which is fast, can scale to large code, and has proven effective in an industrial software engineering scenario. To our knowledge, RacerD is the first inter-procedural, compositional data race detector which has been shown to have non-trivial precision and impact. Due to its compositionality, it can analyze code changes quickly, and this allows it to perform continuous reasoning about a large, rapidly changing codebase as part of deployment within a continuous integration ecosystem. In contrast to previous static race detectors, its design favors reporting high-confidence bugs over ensuring their absence. RacerD has been in deployment for over a year at Facebook, where it has flagged over 2500 issues that have been fixed by developers before reaching production. It has been important in enabling the development of new code as well as fixing old code: it helped support conversion of part of the main Facebook Android app from a single-threaded to a multi-threaded architecture. In this paper we describe RacerD’s design, implementation, deployment and impact.

We introduce a framework for the symbolic verification of epistemic properties of programs expressed in a class of general-purpose programming languages. To this end, we reduce the verification problem to that of satisfiability of first-order formulae in appropriate theories. We prove the correctness of our reduction and we validate our proposal by applying it to two examples: the dining cryptographers problem and the ThreeBallot voting protocol. We put forward an implementation using existing solvers, and report experimental results showing that the approach can perform better than state-of-the-art symbolic model checkers for temporal-epistemic logic.

Intelligent Environments (IE) are a very active area of research and a number of applications are currently being deployed in domains ranging from smart home to e-health and autonomous vehicles. In a number of cases, IE operate together with (or to support) humans, and it is therefore fundamental that IE are thoroughly verified. In this paper we present how a set of techniques and tools developed for the verification of software code can be employed in the verification of IE described by means of event-condition-action rules. In particular, we reduce the problem of verifying key properties of these rules to satisfiability and termination problems that can be addressed using state-of-the-art SMT solvers and program analysers. We introduce a tool called vIRONy that implements these techniques and we validate our approach against a number of case studies from the literature.

We investigate the *model checking* problem for symbolic-heap separation logic with user-defined inductive predicates, i.e., the problem of checking that a given stack-heap memory state satisfies a given formula in this language, as arises e.g. in software testing or runtime verification. First, we show that the problem is *decidable*; specifically, we present a bottom-up fixed point algorithm that decides the problem and runs in exponential time in the size of the problem instance. Second, we show that, while model checking for the full language is EXPTIME-complete, the problem becomes NP-complete or PTIME-solvable when we impose natural syntactic restrictions on the schemata defining the inductive predicates. We additionally present NP and PTIME algorithms for these restricted fragments. Finally, we report on the experimental performance of our procedures on a variety of specifications extracted from programs, exercising multiple combinations of syntactic restrictions.

The notion of warrant or justification is one of the central concepts in formal models of argumentation. The dialectical definition of warrant is expressed in terms of recursive defeat: an argument is warranted if each of its counter-arguments is itself defeated by a warranted counter-argument. However, few complexity results exist on checking whether an argument is warranted in the context of deductive models of argumentation, i.e. models where an argument is a deduction of a claim from a set of premises using some logic. We investigate the computational complexity of checking whether a claim is warranted in propositional argumentation under two natural definitions of warrant and show that it is PSPACE-complete in both cases.

research-article Free Access Share on Minimal refinements of specifications in model and termporal logics Authors: Nikos Gorogiannis School of Computing, University of the West of England, BS 16 1QY, Bristol, UK School of Computing, University of the West of England, BS 16 1QY, Bristol, UKView Profile , Mark Ryan School of Computer Science, University of Birmingham, B15 2TT, Birmingham, UK School of Computer Science, University of Birmingham, B15 2TT, Birmingham, UKView Profile Authors Info & Claims Formal Aspects of ComputingVolume 19Issue 1pp 35–62https://doi.org/10.1007/s00165-006-0014-3Published:01 March 2007Publication History 0citation13DownloadsMetricsTotal Citations0Total Downloads13Last 12 Months8Last 6 weeks0 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

In both scenarios we seek to produce a refinement of a system.Refinement (see e.g.[AL91]) can be viewed as behaviour-containment; if A and B are two systems, then A refines B iff behaviours(A) ⊆ behaviours(B).We will be using transition systems to represent designs of systems (and from now on we will use the terms system and model interchangeably), and as such, an appropriate notion of behaviour is the computation tree.Correspondingly, the set of behaviours exhibited by a transition system is the set of computation trees that results from the unravelling of the transition system.More specific definitions will be given in the following section.In both examples, a refinement of a design is sought.However, refining a system yields an implementation, or a more 'concrete' version of it, but not necessarily a useful one: depending on the formalism used, it is frequently the case that trivial models exist that refine almost every other model.For example, in the case of the database access control system, it is true that an empty transition system does not allow any behaviours at all and, therefore, refines the original one; it is hardly a useful one though.In other words, we are interested in refining the original model but only so much as is necessary in order to satisfy a given guiding property.In this way, behaviours of the original system are only sacrificed if necessary.Thus, instead of just looking for designs that refine the initial one and satisfy the new requirement, we will use refinement to order the designs.We are led, then, to the concept of minimal refinement.Minimal refinement can be used whenever the designer has a model of a system that already circumscribes the allowed behaviours of the system.Then, a new property can be applied and a new design obtained, that satisfies the new requirement, refines the initial design and exhibits as many of its behaviours as possible.A corollary of this is that by using minimal refinement we get automatic preservation of safety properties.The contributions of this paper lie, firstly, in the introduction of the notion of minimal refinement as a method for the stepwise addition of requirements in a model.Secondly, we investigate and prove results concerning several issues around minimal refinement such as the soundness and decidability of algorithms for computing minimal refinements.In what follows we will define this process and study its theoretical and applied aspects.We will focus on representations of designs based on transition systems, and on modal and temporal logics as languages for expressing requirements.We begin by introducing the theoretical background in Sect. 2.Then, we will proceed to formalise these intuitions and define minimal refinement in a precise way in Sect.3. In the same section, the problems that arise from our definition are discussed, and specific technical questions aiming at resolving those problems are specified.These questions are investigated in the context of modal logic in Sect. 4. In the aim of addressing expressiveness issues related to modal logic, we further develop the investigation of these questions into the realm of temporal logic in Sect. 5. Finally, we conclude and summarise the possible avenues for extending the work presented in this paper, in Sect.6.The definitions behind minimal refinement and part of the results presented in Sect. 4 have appeared in [GR02].The results presented in Sect. 5 have appeared in [Gor03]. Preliminaries General backgroundBefore discussing specific logics, we will approach the subject from a higher level.Therefore, let L and M be sets, corresponding to the set of formulae and the set of models of a logic.Let, also, | ⊆ M × L be a satisfaction relation.The class of models that satisfies a formula φ will be denoted by mod(φ).Let ⊆ M × M be a preorder (i.e., a transitive and reflexive relation) on models.The strict counterpart of , denoted by < is defined by the condition M < N iff M N and N M. Given a set S ⊆ M, the minimisation operator is defined in the usual way, min (S) {M ∈ S | ∀ N ∈ S, N < M}.As noted in the introduction, we will be looking at an operation of the form of min (mod(φ)).This operation resembles one often found in the areas known as theory (or belief) change (see, e.g., [Gro88, Dal88, KM89, KM91]) and non-monotonic reasoning (e.g, [KLM90, BMP97, BEF93]), among others.The shared intuition is that, when given a property φ in some logic, instead of selecting all the structures that satisfy φ (mod(φ)) we employ some extra-logical information and treat some models inside mod(φ) in a preferential way.This information takes frequently the form of a relation over models and is usually called a preference relation.Minimal refinements of specifications in modal and temporal logics 419 Modal logicIn Sect.4, we will generally work with a finite set A of propositional variables.The modal language L K of the logic K m on A with m modalities is defined inductively; if p ∈ A then p ∈ L K ; if φ and ψ are in L K then so are ¬ φ and φ ∧ ψ; if φ ∈ L K then 3 i φ ∈ L K for all 1 i m.The usual propositional abbreviations apply as well as the modal 2 i ≡ ¬ 3 i ¬ .The axiomatisation of K m follows. P.Any propositional tautology is an axiom.K. Any formula of the form 2 i (φ → ψ) → (2 i φ → 2 i ψ) with 1 i m is an axiom.Its rules of inference are: MP.Modus ponens: if φ and φ → ψ, then ψ.Nec.Necessitation: if φ, then 2 i φ, for all 1 i m.The logic of K m is defined to be the smallest subset of L K that contains all the instances of the above axioms and is closed under the two rules of inference.The fact that a formula φ ∈ L K is in is denoted by φ.If T is a set of sentences and φ a sentence, then φ is deducible from T , written T φ, if there exists a number n 0 and sentences ψ 1 , . . ., ψ n ∈ T such that ψ 1 ∧ • • • ∧ ψ n → φ.The set T is called consistent if T ⊥ and inconsistent otherwise.The most popular semantics for modal logics is through Kripke models.