Search

Due to ubiquitous use of software services, protecting the confidentiality of private information stored in compute clouds is becoming an increasingly critical problem. Although access control specification languages and libraries provide mechanisms for protecting confidentiality of information, without verification and validation techniques that can assist users in writing policies, complex policy specifications are likely to have errors that can lead to unintended and unauthorized access to data, possibly with disastrous consequences. Current state-of-the art approaches focus on either assertion checking which requires manual specification of assertions (which may not be available or difficult to write) or compare existing policies and report binary results (such as policy 1 is more permissive than policy 2). These techniques however cannot perform quantitative analysis on policies (how much more permissive is policy 1 than policy 2?). It is crucial to develop automated approaches for quantitatively assessing properties of access control policies.Model counting is an emerging area with applications in quantitative analysis. A model counting constraint solver computes the number of solutions for a given constraint within a given bound. Recently, model counting constraint solvers have also been applied to automating quantitative software verification, analysis and security tasks. The goal in quantitative program analysis is not to just give a ``yes'' or ``no'' answer, but to also quantify the result. For example, rather than answering if there is information leakage in a program with a ``yes'' or ``no'' answer, quantitative analysis techniques can compute the amount of information leaked. In this dissertation, we first discuss state-of-the-art techniques for model counting using automata-theoretic techniques and its applications in quantitative program analysis. We then introduce the revamped model counting constraint solver ABC2. Next, we discuss how model counting techniques can be combined with traditional policy analysis approaches to perform quantitative analysis of access control policies, culminating in the open-source policy analysis tool Quacky. At the end, we introduce a quantitative symbolic analysis approach for automated policy repair for fixing overly permissive policies.

One of the most important parts of construction work is the verification of the geometry of the parts of structures and buildings constructed. Today this procedure is often semi- or fully automated. The paper introduces an approach for the automated verification of parts of buildings, by comparing the design of a building (as-planned model), derived from a Building Information Model (BIM) in an Industry Foundation Classes (IFC) exchange format to a terrestrial laser scanning (TLS) point cloud (as-built model). The approach proposed has three main steps. The process begins with the acquisition of information from the as-planned model in the IFC exchange format; the second step is the automated (wall) plane segmentation from the point cloud. In the last step, the two models mentioned are compared to determine the deviations from the design, and the as-built wall flatness quantification is also executed. The potential of the proposed algorithm is shown in a case-study.

International audience; Business process optimization is a strategic activity in organizations because of its potential to increase profit margins and reduce operational costs. One of the main challenges in this activity is concerned with the problem of optimizing allocation and sharing of resources. Companies are continuously adjusting their resources to their needs following different strategies. However, the dynamic provisioning strategies are hard to compare. This paper proposes an automatic analysis technique to evaluate and compare the execution time and resource occupancy of a business process relative to a workload and a provisioning strategy. Four different strategies are presented, which are guided-respectively-by recent resource usage, recent resource request, predicted behavior, and a combination of available strategies. Such analysis is performed on models conforming to an extension of BPMN with quantitative information, including resource availability and constraints. Within this framework, the approach is fully mechanized using a formal and executable specification in the Maude rewriting logic framework, which relies on existing techniques and tools for simulating probabilistic and real-time specifications. The paper includes results on the extensive experimentation that has been carried out for validation purposes.

As the scale and complexity of safety-critical software continue to grow, it is necessary to ensure safety and reliability to avoid minor errors leading to catastrophic disasters. Meantime, the traditional method, such as testing and simulation alone is insufficient to ensure the correctness of systems. This leads to using formal methods to provide sufficient evidence for systems. However, design a high assurance safety-critical system by formal methods is challenging due to the complexity of operating systems. In addition, the traditional interactive theorem prover used in system verification requires hand-written proofs, which are more expensive. Therefore, the efforts of providing a standardized formal framework as well as safety proofs, are notable for the develop a safety-critical system. The purpose of this paper is to provide a safety framework to establish a highly reliable and safety-critical operating system based on the ARINC653 standard, a multilevel and standardized formal model. To verify the functional correctness of this model, we propose a context-based formal proof method for programs. To achieve this goal, we first model 57 core services of ARINC653 and define the high-level requirements as pre-and post-conditions. Then, we construct a set of specification statements a formal axiom system transformed into logical sentences, and the core service model is transformed into a logical sentence sequence to be proved. Finally, a context-based formal proof system for specification correctness is developed. We have verified the correctness of safety-critical operating system core services with this system. Experience shows that the verification system we developed can be achieved the functional correctness of a complete OS with a low implement burden, and that can simplify the difficulty of automated verification and increase the degree of automation of proof.

Population protocols are a well established model of computation by anonymous, identical finite state agents. A protocol is well-specified if from every initial configuration, all fair executions reach a common consensus. The central verification question for population protocols is the well-specification problem: deciding if a given protocol is well-specified. Esparza et al. have recently shown that this problem is decidable, but with very high complexity: it is at least as hard as the Petri net reachability problem, which is EXPSPACE-hard, and for which only algorithms of non-primitive recursive complexity are currently known. In this paper we introduce the class WS3 of well-specified strongly-silent protocols and we prove that it is suitable for automatic verification. More precisely, we show that WS3 has the same computational power as general well-specified protocols, and captures standard protocols from the literature. Moreover, we show that the membership problem for WS3 reduces to solving boolean combinations of linear constraints over N. This allowed us to develop the first software able to automatically prove well-specification for all of the infinitely many possible inputs., 29 pages, 1 figure

Go is an increasingly-popular systems programming language targeting, especially, concurrent and distributed systems. Go differentiates itself from other imperative languages by offering structural subtyping and lightweight concurrency through goroutines with message-passing communication. This combination of features poses interesting challenges for static verification, most prominently the combination of a mutable heap and advanced concurrency primitives. We present Gobra, a modular, deductive program verifier for Go that proves memory safety, crash safety, data-race freedom, and user-provided specifications. Gobra is based on separation logic and supports a large subset of Go. Its implementation translates an annotated Go program into the Viper intermediate verification language and uses an existing SMT-based verification backend to compute and discharge proof obligations., Lecture Notes in Computer Science, 12759, ISSN:0302-9743, ISSN:1611-3349, Computer Aided Verification, 33rd International Conference, CAV 2021, Virtual Event, July 20–23, 2021, Proceedings, Part I, ISBN:978-3-030-81684-1, ISBN:978-3-030-81685-8

International audience; The masking countermeasure is among the most powerful countermeasures to counteract side-channel attacks. Leakage models have been exhibited to theoretically reason on the security of such masked implementations. So far, the most widely used leakage model is the probing model defined by Ishai, Sahai, and Wagner at (CRYPTO 2003). While it is advantageously convenient for security proofs, it does not capture an adversary exploiting full leakage traces as, e.g., in horizontal attacks. Those attacks target the multiple manipulations of the same share to reduce noise and recover the corresponding value. To capture a wider class of attacks another model was introduced and is referred to as the random probing model. From a leakage parameter p, each wire of the circuit leaks its value with probability p. While this model much better reflects the physical reality of side channels, it requires more complex security proofs and does not yet come with practical constructions. In this paper, we define the first framework dedicated to the random probing model. We provide an automatic tool, called VRAPS, to quantify the random probing security of a circuit from its leakage probability. We also formalize a composition property for secure random probing gadgets and exhibit its relation to the strong non-interference (SNI) notion used in the context of probing security. We then revisit the expansion idea proposed by Ananth, Ishai, and Sahai (CRYPTO 2018) and introduce a compiler that builds a random probing secure circuit from small base gadgets achieving a random probing expandability property. We instantiate this compiler with small gadgets for which we verify the expected properties directly from our automatic tool. Our construction can tolerate a leakage probability up to 2 −8 , against 2 −25 for the previous construction, with a better asymptotic complexity.

International audience; Cryptographic implementations deployed in real world devices often aim at (provable) security against the powerful class of side-channel attacks while keeping reasonable performances. Last year at Asiacrypt, a new formal verification tool named tightPROVE was put forward to exactly determine whether a masked implementation is secure in the well-deployed probing security model for any given security order t. Also recently, a compiler named Usuba was proposed to automatically generate bitsliced implementations of cryptographic primitives.This paper goes one step further in the security and performances achievements with a new automatic tool named Tornado. In a nutshell, from the high-level description of a cryptographic primitive, Tornado produces a functionally equivalent bitsliced masked implementation at any desired order proven secure in the probing model, but additionally in the so-called register probing model which much better fits the reality of software implementations. This framework is obtained by the integration of Usuba with tightPROVE+, which extends tightPROVE with the ability to verify the security of implementations in the register probing model and to fix them with inserting refresh gadgets at carefully chosen locations accordingly.We demonstrate Tornado on the lightweight cryptographic primitives selected to the second round of the NIST competition and which somehow claimed to be masking friendly. It advantageously displays performances of the resulting masked implementations for several masking orders and prove their security in the register probing model.

The swift and continuous evolution of mobile devices is encouraging both private and public organizations to adopt the Bring Your Own Device (BYOD) paradigm. As a matter of fact, the BYOD paradigm drastically reduces costs and increases productivity by allowing employees to carry out business tasks on their personal devices. However, it also increases the security concerns, since a compromised device could disruptively access the resources of the organization. The current mobile application distribution model based on application markets does not cope with this issue. In a previous work the concept of secure meta-market has been introduced as a mean to distribute mobile applications always guaranteed to comply with any given BYOD policy. This is achieved through a suitable combination of static analysis (i.e.model checking) and code instrumentation techniques. Although crucial, enforcing security policies over individual applications is not sufficient in general. Indeed, several well documented threats arise from the malicious interaction among applications which are harmless if isolated. In this paper, a novel technique for the security verification of groups of mobile app is proposed. The approach relies on partial model checking (PMC) to extend the existing security guarantees to groups of applications. The experimental results demonstrate the viability of the approach. Moreover, we show through a case study that even a fairly simple security policy can be violated by applications which are compliant if considered one by one. A practical approach to the validation of groups of mobile apps is presented.The approach relies on partial model checking for mitigating state explosion.Experiments on real applications show that the technique scales on real systems.The solution is integrated with a prototype of the Secure Meta-Market (SMM).

What if we designed a tool to automatically generate a dynamical transition system for the formal specification of mechanical systems subject to multiple impacts, contacts and discontinuous friction? Such a tool would represent an advance in the description and simulation of these complex systems. This is precisely what this paper offers: Dyverse Rigid Body Toolbox (DyverseRBT). This tool requires a sufficiently expressive computational model that can accurately describe the behaviour of the system as it evolves over time. For this purpose, we propose an alternative abstraction of multi-rigid-body mechanical systems with multiple contacts as an extended version of the classical hybrid automaton, which we call multi-rigid-body hybrid automaton. One of the chief characteristics of the multi-rigid-body hybrid automaton is the inclusion of computation nodes to encode algorithms to calculate the contact forces. The computation nodes consist of a set of non-dynamical discrete locations, discrete transitions and guards between these locations, and resets on transitions. They can account for the energy transfer not explicitly considered within the rigid-body formalism. The proposed modelling framework is well-suited for the automated verification of dynamical properties of realistic mechanical systems. We show this by the falsification of safety properties over the transition system generated by DyverseRBT.

This paper presents an approach for the modeling and analysis of resource allocation for business processes. It enables the automatic computation of measures for precisely identifying and optimizing the allocation of resources in business processes, including resource usage over time. The proposed analysis, especially suited to support decision-making strategies, is illustrated with a case study of a parcel ordering and delivery by drones that is developed throughout the paper. The paper comprises an encoding of a significant and expressive subset of the Business Process Model and Notation (BPMN) in rewriting logic, an executable logic of concurrent change that can naturally deal with state and with concurrent computations. The encoding is by itself a formal semantics and interpreter of the BPMN subset that captures all concurrent behavior and thus is used to simulate the concurrent evolution of any business process with a given number of resources and replicas.

Scope of Research. This paper deals with the problem of design space exploration for a particular class of networked embedded systems called Real-Time Location Systems (RTLS). Methods. The paper contains a clear and detailed plan of an ongoing research and could be considered as a review, a vision and a statement of objectives. Analytical and formal methods, simulation and automated verification will be involved in the research. Main Results. Analysis of the state of the art (current design flow, existing simulation tools and verification techniques) has revealed several limitations for performing efficient design space exploration of RTLS, especially for safety-critical applications. The review part of the paper also contains a clear problem statement. The main outcome of this research is the proposed vision of a novel methodology for determining the best-suited technology and its configuration from the space of potential solutions. In particular, it is planned to extend an existing simulation framework and apply automated verification techniques. The latter will be used for checking simulation results and also for exploring different system configuration alternatives, that is, to optimize the design, which is a novel approach. A case study for validating the methodology is also proposed. Practical Significance. The proposed methodology will highly increase the breadth of design space exploration of RTLS as well as the confidence on taken design decisions. It will also contribute to optimizing the design.

We consider the well-known Sliding Window Protocol which provides reliable and efficient transmission of data over unreliable channels. A formal proof of correctness for this protocol faces substantial difficulties caused by a high degree of parallelism which creates a significant potential for errors. Here we consider a version of the protocol that is based on selective repeat of frames. The specification of the protocol by a state machine and its safety property are represented in the language of the verification system PVS. Using the PVS system, we give an interactive proof of this property of the Sliding Window Protocol.

International audience; In contrast to other IT systems, industrial systems often do not only require classical properties like data confidentiality or authentication of the communication, but have special needs due to their interaction with physical world. For example, the reordering or deletion of some commands sent to a machine can cause the system to enter an unsafe state with potentially catastrophic effects. To prevent such attacks, the integrity of the message flow is necessary. We provide a formal definition of Flow Integrity. We apply our framework to two well-known industrial protocols: OPC-UA and MODBUS. Using TAMARIN, a cryptographic protocol verification tool, we confirm that most of the secure modes of these protocols ensure Flow Integrity given a resilient network. However, we also identify a weakness in a supposedly secure version of MODBUS.

In this paper, we combine formal modeling and analysis of infrastructures of organizations with sociological explanation to provide a framework for insider threat analysis. We use the higher order logic (HOL) proof assistant Isabelle/HOL to support this framework. In the formal model, we exhibit and use a common trick from the formal verification of security protocols, showing that it is applicable to insider threats. We introduce briefly a three-step process of social explanation, illustrating that it can be applied fruitfully to the characterization of insider threats. We introduce the insider theory constructed in Isabelle that implements this process of social explanation. To validate that the social explanation is generally useful for the analysis of insider threats and to demonstrate our framework, we model and verify the insider threat patterns of entitled independent and Ambitious Leader in our Isabelle/HOL framework.

International audience; Business processes support the modeling and the implementation of software as workflows of local and inter-process activities. Taking over structuring and composition, evolution has become a central concern in software development. We advocate it should be taken into account as soon as the modeling of business processes, which can thereafter be made executable using process engines or model-to-code transformations. We show here that business process evolution needs formal analysis in order to compare different versions of processes, identify precisely the differences between them, and ensure the desired consistency. To reach this objective, we first present a model transformation from the BPMN standard notation to the LNT process algebra. We then propose a set of relations for comparing business processes at the formal model level. With reference to related work, we propose a richer set of comparison primitives supporting renaming, refinement, property- and context-awareness. Thanks to an implementation of our approach that can be used through a Web application, we put the checking of evolution within the reach of business process designers.

International audience; Fault-tolerant distributed algorithms play an important role in many critical/high-availability applications. These algorithms are notoriously difficult to implement correctly, due to asynchronous communication and the occurrence of faults, such as the network dropping messages or computers crashing. We introduce PSYNC, a domain specific language based on the Heard-Of model, which views asynchronous faulty systems as synchronous ones with an adversarial environment that simulates asyn-chrony and faults by dropping messages. We define a runtime system for PSYNC that efficiently executes on asynchronous networks. We formalise the relation between the runtime system and PSYNC in terms of observational refinement. This high-level synchronous abstraction introduced by PSYNC simplifies the design and implementation of fault-tolerant distributed algorithms and enables automated formal verification. We have implemented an embedding of PSYNC in the SCALA programming language with a runtime system for partially synchronous networks. We show the applicability of PSYNC by implementing several important fault-tolerant distributed algorithms and we compare the implementation of consensus algorithms in PSYNC against implementations in other languages in terms of code size, runtime efficiency, and verification.

The coordination modelling language Paradigm addresses collaboration between components in terms of dynamic constraints. Within a Paradigm model, component dynamics are consistently specified at various levels of abstraction. The operational semantics of Paradigm is given. For a large, general subclass of Paradigm models a translation into process algebra is provided. Once expressed in process algebra, relying on a correctness result, Paradigm models are amenable to process algebraic reasoning and to verification via the mCRL2 toolset. Examples of a scheduling problem illustrate the approach.

This paper describes a general technique to identify control flow errors in parallel programs, which can be automated into a compiler. The compiler builds a system of linear equations that describes the global control flow of the whole program. Solving these equations using standard techniques of linear algebra can locate a wide range of control flow bugs at compile time. This paper also describes an implementation of this control flow analysis technique in a prototype compiler for a well-known parallel programming language. In contrast to previous research in automated parallel program analysis, our technique is efficient for large programs, and does not limit the range of language features.

Consensus is at the heart of fault-tolerant distributed computing systems. Much research has been devoted to developing algorithms for this particular problem. This paper presents a semi-automatic verification approach for asynchronous consensus algorithms, aiming at facilitating their development. Our approach uses model checking, a widely practiced verification method based on state traversal. The challenge here is that the state space of these algorithms is huge, often infinite, thus making model checking infeasible. The proposed approach addresses this difficulty by reducing the verification problem to small model checking problems that involve only single phases of algorithm execution. Because a phase consists of a small, finite number of rounds, bounded model checking, a technique using satisfiability solving, can be effectively used to solve these problems. The proposed approach allows us to model check several consensus algorithms up to around 10 processes.

This paper presents a methodology for automated modular verification of C programs against specifications written in separation logic. The distinguishing features of the approach are representation of the C memory model in separation logic by means of rewrite rules suitable for automation and the careful integration of an SMT solver behind the separation logic prover to guide the proof search.

International audience; This paper proposes a framework that automatically checks and configures data security in Web Services starting from high level business requirements. We consider BPEL-based composed Web Services. BPEL processes and initial security parameters are represented as component-based models labeled with security annotations. These models are formal and enable automated analysis and synthesis of security configurations, under the guidance of the service designer. The security property considered is the non-interference. The overall approach is practical since security is defined separately from functional processes and automatically verified. We illustrate its utility to solve intricate security problems using a smart grid application.

Automated verification of operating system kernels is a challenging problem, partly due to the use of shared mutable data structures. In this paper, we show how we can automatically verify memory safety and functional correctness properties of the task scheduler component of the FreeRTOS kernel using the verification system Hip/Sleek. We show how some of Hip/Sleek features such as user-defined predicates and lemmas make the specifications highly expressive and the verification process viable. To the best of our knowledge, this is the first code-level verification of memory safety and functional correctness properties of the FreeRTOS scheduler. The outcome of our experiment confirms that Hip/Sleek can indeed be used to verify code that is used in production. Moreover, since the properties that we verify are quite general, we envisage that the same approach can be adopted to verify components of other operating systems.

International audience; This paper proposes a formal framework for studying information flow security in component-based systems. The security policy is defined and verified from the early steps of the system design. Two kinds of non-interference properties are formally introduced and for both of them, sufficient conditions that ensures and simplifies the automated verification are proposed. The verification is compositional, first locally, by checking the behavior of every atomic component and then globally, by checking the inter-components communication and coordination. The potential benefits are illustrated on a concrete case study about constructing secure heterogeneous distributed systems.

Although Prolog is (still) the most widely used logic language, it suffers from a number of drawbacks which prevent it from being truely declarative. The nondeclarative features such as the depth-first search rule are nevertheless necessary to make Prolog reasonably efficient. Several authors have proposed methodologies to reconcile declarative programming with the algorithmic features of Prolog. The idea is to analyse the logic program with respect to a set of properties such as modes, types, sharing, termination, and the like in order to ensure that the operational behaviour of the Prolog program complies with its logic meaning. Such analyses are tedious to perform by hand and can be automated to some extent. This paper presents a state-of-the-art analyser which allows one to integrate many individual analyses previously proposed in the literature as well as new ones. Conceptually, the analyser is based on the notion of abstract sequence which makes it possible to collect all kinds of desirable information, including relations between the input and output sizes of terms, multiplicity, and termination.

International audience; Many companies have adopted MDD for developing their software systems. Several studies have reported on such industrial experiences by discussing the effects of MDD and the issues that still need to be addressed. However, only a few studies have discussed using automated verification of industrial model transformations. We previously demonstrated how transformations can be used to migrate GM legacy models to AUTOSAR models. In this study, we investigate using automated verification for such industrial transformations. We report on applying an automated verification approach to the GM-to-AUTOSAR transformation that is based on checking the satisfiability of a relational transformation representation, or a transformation model, with respect to well-formedness OCL constraints. An implementation of this approach is available as a prototype for the ATL language. We present the verification results of this transformation and discuss the practicality of using such tools on industrial size problems.

Date of Conference: 18-26 May 2013 Conference name: 2nd International Workshop on Software Engineering Challenges for the Smart Grid (SE4SG), 2013 Smart grid applications are implemented and tested with simulation frameworks as the developers usually do not have access to large sensor networks to be used as a test bed. The developers are forced to map the implementation onto these frameworks which results in a deviation between the architecture and the code. On its turn this deviation makes it hard to verify behavioral constraints that are described at the architectural level. We have developed the ConArch toolset to support the automated verification of architecture-level behavioral constraints. A key feature of ConArch is programmable mapping for architecture to the implementation. Here, developers implement queries to identify the points in the target program that correspond to architectural interactions. ConArch generates runtime observers that monitor the flow of execution between these points and verifies whether this flow conforms to the behavioral constraints. We illustrate how the programmable mappings can be exploited for verifying behavioral constraints of a smart grid application that is implemented with two simulation frameworks. © 2013 IEEE.

AVoCS 2014, the 14th International Conference on Automated Verification of Critical Systems has been hosted by the University of Twente, and has taken place in Enschede, Netherlands, on 24-26 September, 2014. The aim of the AVoCS series is to contribute to the interaction and exchange of ideas among members of the international research community on tools and techniques for the verification of critical systems. The subject is to be interpreted broadly and inclusively. It covers all aspects of automated verification, including model checking, theorem proving, abstract interpretation, and refinement pertaining to various types of critical systems (safety-critical, security-critical, business-critical, performance-critical, etc.).

jStar is a tool for automatically verifying Java programs. It uses separation logic to support abstract reasoning about object specifications. jStar can verify a number of challenging design patterns, including Subject/Observer, Visitor, Factory and Pooling. However, to use jStar one has to deal with a family of command-line tools that expect specifications in separate files and diagnose the errors by inspecting the text output from these tools. In this paper we present a plug-in, called jStar-eclipse, allowing programmers to use jStar from within Eclipse IDE. Our plug-in allows writing method contracts in Java source files in form of Java annotations. It automatically translates Java annotations into jStar specifications and propagates errors reported by jStar back to Eclipse, pinpointing the errors to the locations in source files. This way the plug-in ensures an overall better user experience when working with jStar. Our end goal is to make automated verification based on separation logic accessible to a broader audience.

We provide a survey of the state of the art ofrational verification: the problem of checking whether a given temporal logic formulaϕis satisfied in some or all game-theoretic equilibria of a multi-agent system – that is, whether the system will exhibit the behaviorϕrepresents under the assumption that agents within the system act rationally in pursuit of their preferences. After motivating and introducing the overall framework of rational verification, we discuss key results obtained in the past few years as well as relevant related work in logic, AI, and computer science.

International audience; Security APIs, key servers and protocols that need to keep the status of transactions, require to maintain a global, non-monotonic state, e.g., in the form of a database or register. However, most existing automated verification tools do not support the analysis of such stateful security protocols – sometimes because of fundamental reasons, such as the encoding of the protocol as Horn clauses, which are inherently monotonic. A notable exception is the recent tamarin prover which allows specifying protocols as multiset rewrite (msr) rules, a formalism expressive enough to encode state. As multiset rewriting is a " low-level " specification language with no direct support for concurrent message passing, encoding protocols correctly is a difficult and error-prone process. We propose a process calculus which is a variant of the applied pi calculus with constructs for manipulation of a global state by processes running in parallel. We show that this language can be translated to msr rules whilst preserving all security properties expressible in a dedicated first-order logic for security properties. The translation has been implemented in a prototype tool which uses the tamarin prover as a backend. We apply the tool to several case studies among which a simplified fragment of PKCS#11, the Yubikey security token, and an optimistic contract signing protocol.

We consider past pushdown timed automata that are discrete pushdown timed automata with past formulas as enabling conditions. Using past formulas allows a past pushdown timed automaton to access the past values of the finite state variables in the automaton. We prove that the reachability (i.e., the set of reachable configurations from an initial configuration) of a past pushdown timed automaton can be accepted by a nondeterministic reversal-bounded counter-machine augmented with a pushdown stack (i.e., a reversal-bounded NPCM). By using the known fact that the emptiness problem for reversal-bounded NPCMs is decidable, we show that model-checking past pushdown timed automata against Presburger safety properties on discrete clocks and stack word counts is decidable. We also investigate the reachability problem for a class of transition systems under some fairness constraints in the form of generalized past formulas. Finally, we present an example ASTRAL specification to demonstrate the usefulness of the results.

Distributed groupware systems provide computer support for manipulating objects such as a text document or a filesystem, shared by two or more geographically separated users. Data replication is a technology to improve performance and availability of data in distributed groupware systems. Indeed, each user has a local copy of the shared objects, upon which he may perform updates. Locally executed updates are then transmitted to the other users. This replication potentially leads, however, to divergent (i.e. different) copies. In this respect, Operational Transformation (OT) algorithms are applied for achieving convergence of all copies, i.e. all users view the same objects. Using these algorithms users can exchange their updates in any order since the convergence should be ensured in all cases. However, the design of such algorithms is a difficult and error-prone activity since building the correct updates for maintaining good convergence properties of the local copies requires examining a large number of situations. In this paper, we present the modelling and deductive verification of OT algorithms with algebraic specifications. We show in particular that many OT algorithms in the literature do not satisfy convergence properties unlike what was stated by their authors.

Despite their popularity and importance, pointer-based programs remain a major challenge for program verification. In recent years, separation logic has emerged as a contender for formal reasoning of pointer-based programs. Recent works have focused on specialized provers that are mostly based on fixed sets of predicates. In this paper, we propose an automated verification system for ensuring the safety of pointer-based programs, where specifications handled are concise, precise and expressive. Our approach uses user-definable predicates to allow programmers to describe a wide range of data structures with their associated shape, size and bag (multi-set) properties. To support automatic verification, we design a new entailment checking procedure that can handle well-founded predicates (that may be recursively defined) using unfold/fold reasoning. We have proven the soundness and termination of our verification system and built a prototype system to demonstrate the viability of our approach.