ABSTRACT. We present a black-box inprocessor for the partially weighted maximum satisfiability problem, which extends any given MaxSAT solver with inprocessing capabilities without modifying the core solver. Our approach combines the well-established cube-and-conquer technique with classical dynamic programming over a tree decomposition of the formula. While the first technique is limited in the size of the cubes it can handle, the second technique is elementary limited by the treewidth of the input. By combining both paradigms, we are able to handle significantly bigger cubes in instances with a treewidth of over a thousand, all without suffering performance losses on unstructured instances.

Through an extensive experimental study, we demonstrate the efficiency of our approach in enhancing established implementations of various standard algorithms for MaxSAT. Our results showcase that structure-guided cube-and-conquer can serve as a general black-box inprocessor for MaxSAT, making it a valuable addition to the MaxSAT toolbox.

ABSTRACT. The Boolean satisfiability problem holds a significant place in computer science, finding applications across various domains. This problem entails the quest for a truth assignment to a given Boolean formula that either validates it or conclusively proves its impossibility. An indispensable element influencing the efficacy of tools designed for tackling this challenge, known as SAT solvers, is the choice of an appropriate initialization strategy. This strategy encompasses the assignment of initial values, or polarities, to the variables before starting the search process.

A well-crafted initialization strategy possesses the capability to curtail the search space and minimize the number of conflicts and backtracks by ensuring that variables are assigned values that are likely to satisfy the formula from the outset.

This paper introduces an innovative initialization approach founded on genetic algorithms, which are evolutionary algorithms inspired by the principles of natural selection and reproduction. Our approach executes a genetic algorithm on the given formula, persisting until it discovers a satisfying assignment or meets predetermined termination criteria.

Subsequently, it furnishes the satisfying assignment in case of success; otherwise, it employs the best assignment (that satisfies the highest number of clauses) to initialize the variables' polarities for the SAT solver.

ABSTRACT. Solutions to differential equations, which are used to model physical systems, are computed numerically by solving a set of discretized equations. This set of discretized equations is reduced to a large linear system, whose solution is typically found using an iterative solver. We start with an initial guess, $x_0$, and iterate the algorithm to obtain a sequence of solution vectors, $x_k$, which are approximations to the exact solution of the linear system, $x$. The iterative algorithm is said to converge to $x$, in the field of reals, if and only if $x_k$ converges to $x$ in the limit of $k \to \infty$.

In this paper, we formally prove the asymptotic convergence of a particular class of iterative methods called the stationary iterative methods, in the Coq theorem prover. We formalize the necessary and sufficient conditions required for the iterative convergence, and extend this result to two classical iterative methods: the Gauss--Seidel method and the Jacobi method. For the Gauss--Seidel method, we also formalize a set of easily testable conditions for iterative convergence, called the Reich theorem, for a particular matrix structure, and apply this on a model problem of the one-dimensional heat equation. We also apply the main theorem of iterative convergence to prove convergence of the Jacobi method on the model problem.

We leverage recent developments of the Coq linear algebra, Coquelicot's real analysis library and the MathComp library for our formalization.

ABSTRACT. Probabilistic model checking provides formal guarantees for stochastic models relating to a wide range of quantitative properties. But this is typically with respect to the expected value of these quantities, which can mask important aspects of the full probability distribution. We propose a distributional extension of probabilistic model checking, for discrete-time Markov chains (DTMCs) and Markov decision processes (MDPs). We formulate distributional queries, which can reason about a variety of distributional measures, such as variance, value-at-risk or conditional value-at-risk, for the accumulation of reward or cost until a co-safe linear temporal logic formula is satisfied. For DTMCs, we propose a method to compute the full distribution to an arbitrary level of precision. For MDPs, we approximate the optimal policy using distributional value iteration. We implement our techniques and investigate their performance and scalability across a range of large benchmark models.

ABSTRACT. Programming errors in software applications may produce plausible yet erroneous results, without providing a clear indication of failure. This happens, for instance, when certain inputs have a disproportionate impact on the program result. To address this issue, we propose a novel quantitative static analysis for determining the impact of inputs on the program computations, parametrized in the definition of impact. This static analysis employs an underlying abstract backward analyzer and computes a sound over-approximation of the impact of program inputs, providing valuable insights into how the analyzed program handles them. We implement a proof-of-concept static analyzer to demonstrate potential applications.

ABSTRACT. Derecho is a C++ framework for distributed programming leveraging high performance communication primitives such as RDMA. At its core is the shared state table (SST), a replicated data structure that supports efficient protocols for consensus and group membership. Our aim is to formalize the reasoning principles articulated by the designers, which focus on knowledge and monotonicity, as basis for highly assured high performance distributed applications. To this end we develop a high level model that exposes the SST principles in an application-friendly way. We use the model to specify and verify a re-implementation in C of the SST API. We validate the specifications by verifying simple applications that embody key parts of the Derecho protocols. The development is carried out using VST and Coq. This lays groundwork for verification of the full Derecho protocols and applications built on them.

ABSTRACT. Self-balancing binary search trees are essential in computer science for their versatility and efficient management of ordered data. While the conceptual foundation of a particular tree might be consistent, multiple implementations can exist. This diversity highlights the critical importance of verifying the correctness of a specific implementation. With this perspective, this paper shifts focus to the scapegoat tree, a type of self-balancing tree, prized for its operational simplicity. Utilizing the formal verification tool, Dafny, we undertake a rigorous examination of a scapegoat tree implementation. Through Dafny's comprehensive specification and verification techniques, we prove the correctness of its core operations within our chosen implementation. We also summarized our user experience with Dafny, presenting several techniques that can enhance the efficiency of the proof process.

ABSTRACT. TLA+ is a formal specification language for modelling systems and programs. While TLA+ allows writing specifications involving real numbers, its existing tool support does not currently extend to automating real arithmetic proofs. This functionality is crucial for proving properties of hybrid systems, which may exhibit both continuous and discrete behaviours. In this paper, we address this limitation by enabling support for deciding first-order real arithmetic formulas (involving only polynomials). Specifically, we update the typed and untyped encodings in the TLA+ Proof System (TLAPS) to support reals and basic real arithmetic operations and implement them in the TLA+ proof manager. The latter generates assertions in SMT-LIB and directs them to a selected backend (currently the Z3 SMT solver, which supports the theory of nonlinear real arithmetic). We present this new functionality with a safety verification example featuring a hybrid system.

ABSTRACT. Model-based software design has coexisted with more formal property-based approaches to software design and verification without much interplay. Generally, models provide a way to capture the behavior of physical artifacts, high-level designs, as well as good design practice in the form of reusable design patterns. Formal specifications focus on intensional patterns of temporal and state properties often without explicit computational content. In this paper we explore a formal framework called model refinement that allows combining the strengths of both approaches. Model refinement provides automated tools for incorporating properties into models such that the resulting model is correct-by-construction. Moreover, software design research is often divided into approaches to functional program design and reactive system design. Model refinement provides a unified framework for mechanizing the design of both functions and reactive systems.

In model refinement, a model is treated as an overapproximation of the desired behavior of a system or program; that is, the behaviors of a model are assumed to be a superset of the desired behaviors. Logical properties are specified to further constrain behaviors, with the intent that the model together with specified properties provides a formal specification of the desired system or program. It is our experience that combining models and properties in a formal specification provides a simpler and more natural way to capture the requirements on a software artifact.

Given a model M that overapproximates required system behaviors and a required property P, the goal of model refinement is to generate formal refinements of M so as to eliminate behaviors that do not satisfy P. Given M and P, a definite/Horn-like constraint system is defined whose solutions are models that are both refinements of M and satisfy P. Solutions are computed by fixpoint iteration. For simplicity of exposition we focus on the enforcement of safety properties.

We developed a fully automatic prototype implementation of model refinement based on the Z3 SMT solver. It has been used to solve a variety of system and algorithm design problems.

ABSTRACT. We propose an efficient symbolic control synthesis algorithm for equivariant continuous-time dynamical systems to satisfy reach-avoid specifications. The algorithm exploits dynamical symmetries to construct lean abstractions to avoid redundant computations during synthesis. Our proposed algorithm adds another layer of abstraction over the common grid-based discrete abstraction before solving the synthesis problem. It combines each set of grid cells that are at a similar relative position from the targets and nearby obstacles, defined by the symmetries, into a single abstract state. It uses this layer of abstraction to guide the order by which actions are explored during synthesis over the grid-based abstraction. We demonstrate the potential of our algorithm by synthesizing a reach-avoid controller for a 3-dimensional ship model with translation and rotation symmetries in the special Euclidean group SE(2). Code is available at: https://github. com/HusseinSibai/symmetric_control_synthesis/tree/public.

ABSTRACT. The integration of Unmanned Aircraft Systems (UAS) in the National Airspace System (NAS) for Urban Air Mobility (UAM) opera- tions will create the need to develop robust, efficient, and verifiable tools and techniques for UAS Traffic Management (UTM). In this paper, we present a novel approach for strategic detection and elimination of air- borne conflicts using Satisfiability Modulo Theories (SMT) solvers. Our approach takes a flight plan for an ownship, a set of immutable flight plans for traffic aircraft, and a set of constraints, and then returns a flight plan for the ownship that satisfies all constraints and is also con- flict free with respect to the traffic aircraft. The constraints can relate to operational, business, or other aspects which must be considered while setting up the conflict elimination task as a constraint satisfaction prob- lem. We present simulations of our approach using dReal, an SMT solver that is specialized for solving non-linear real function problems, showing promising results.