arXiv subjects

Panagiotis Manolios

Publications and source records attributed to Panagiotis Manolios.

At least 19 recordsLinked to original sources

arXiv2025

An ACL2s Interface to Z3

We present Lisp-Z3, an extension to the ACL2s systems programming framework (ASPF) that supports the use of the Z3 satisfiability modulo theories (SMT) solver. Lisp-Z3 allows one to develop tools written using the full feature set of Common Lisp that can use both ACL2/s (either ACL2 or ACL2s) and Z3 as services, combining the power of SMT and interactive theorem proving. Lisp-Z3 is usable by anyone who would like to interact with Z3 from Common Lisp, as it does not depend on the availability of ACL2/s. We discuss the use of Lisp-Z3 in three applications. The first is a Sudoku solver. The second is SeqSolve, a string solver which solved a larger number of benchmark problems more quickly than any other existing solver at the time of its publishing. Finally, Lisp-Z3 was also used in the context of hardware-in-the-loop fuzzing of wireless routers, where low latency was an important goal. The latter two applications leveraged the ability of Lisp-Z3 to integrate Z3 with ACL2s code. We have further plans to use Lisp-Z3 inside of ACL2s to provide more powerful automated support for dependent types, and in particular more efficient generation of counterexamples to properties involving dependent types. This paper describes the usage and implementation of Lisp-Z3, as well as an evaluation of its use in the aforementioned applications.

cs.LO↗

arXiv2025

An Enumerative Embedding of the Python Type System in ACL2s

Python is a high-level interpreted language that has become an industry standard in a wide variety of applications. In this paper, we take a first step towards using ACL2s to reason about Python code by developing an embedding of a subset of the Python type system in ACL2s. The subset of Python types we support includes many of the most commonly used type annotations as well as user-defined types comprised of supported types. We provide ACL2s definitions of these types, as well as defdata enumerators that are customized to provide code coverage and identify errors in Python programs. Using the ACL2s embedding, we can generate instances of types that can then be used as inputs to fuzz Python programs, which allows us to identify bugs in Python code that are not detected by state-of-the-art Python type checkers. We evaluate our work against four open-source repositories, extracting their type information and generating inputs for fuzzing functions with type signatures that are in the supported subset of Python types. Note that we only use the type signatures of functions to generate inputs and treat the bodies of functions as black boxes. We measure code coverage, which ranges from about 68% to more than 80%, and identify code patterns that hinder coverage such as complex branch conditions and external file system dependencies. We conclude with a discussion of the results and recommendations for future work.

cs.PL↗

arXiv2025

A Formalization of the Correctness of the Floodsub Protocol

Floodsub is a simple, robust and popular peer-to-peer publish/subscribe (pubsub) protocol, where nodes can arbitrarily leave or join the network, subscribe to or unsubscribe from topics and forward newly received messages to all of their neighbors, except the sender or the originating peer. To show the correctness of Floodsub, we propose its specification: Broadcastsub, in which implementation details like network connections and neighbor subscriptions are elided. To show that Floodsub does really implement Broadcastsub, one would have to show that the two systems have related infinite computations. We prove this by reasoning locally about states and their successors using Well-Founded Simulation (WFS). In this paper, we focus on the mechanization of a proof which shows that Floodsub is a simulation refinement of Broadcastsub using WFS. To the best of our knowledge, ours is the first mechanized refinement-based verification of a real world pubsub protocol.

cs.LO↗

arXiv2025

Proceedings 19th International Workshop on the ACL2 Theorem Prover and Its Applications

The ACL2 Workshop series is the major technical forum for users of the ACL2 theorem proving system to present research related to the ACL2 theorem prover and its applications. ACL2 is an industrial-strength automated reasoning system, the latest in the Boyer-Moore family of theorem provers. The 2005 ACM Software System Award was awarded to Boyer, Kaufmann, and Moore for their work on ACL2 and the other theorem provers in the Boyer-Moore family.

cs.LO↗

arXiv2025

Global Microprocessor Correctness in the Presence of Transient Execution

Correctness for microprocessors is generally understood to be conformance with the associated instruction set architecture (ISA). This is the basis for one of the most important abstractions in computer science, allowing hardware designers to develop highly-optimized processors that are functionally "equivalent" to an ideal processor that executes instructions atomically. This specification is almost always informal, e.g., commercial microprocessors generally do not come with conformance specifications. In this paper, we advocate for the use of formal specifications, using the theory of refinement. We introduce notions of correctness that can be used to deal with transient execution attacks, including Meltdown and Spectre. Such attacks have shown that ubiquitous microprocessor optimizations, appearing in numerous processors for decades, are inherently buggy. Unlike alternative approaches that use non-interference properties, our notion of correctness is global, meaning it is single specification that: formalizes conformance, includes functional correctness and is parameterized by an microarchitecture. We introduce action skipping refinement, a new type of refinement and we describe how our notions of refinement can be decomposed into properties that are more amenable to automated verification using the the concept of shared-resource commitment refinement maps. We do this in the context of formal, fully executable bit- and cycle-accurate models of an ISA and a microprocessor. Finally, we show how light-weight formal methods based on property-based testing can be used to identify transient execution bugs.

cs.CR↗

arXiv2024

Synthesizing Scoring Functions for Rankings Using Symbolic Gradient Descent

Given a relation and a ranking of its tuples, but no information about the ranking function, we are interested in synthesizing simple scoring functions that reproduce the ranking. Our system RankHow identifies linear scoring functions that minimize position-based error, while supporting flexible constraints on their weights. It is based on a new formulation as a mixed-integer linear program (MILP). While MILP is NP-hard in general, we show that RankHow is orders of magnitude faster than a tree-based algorithm that guarantees polynomial time complexity (PTIME) in the number of input tuples by reducing the MILP problem to many linear programs (LPs). We hypothesize that this is caused by 2 properties: First, the PTIME algorithm is equivalent to a naive evaluation strategy for the MILP program. Second, MILP solvers rely on advanced heuristics to reason holistically about the entire program, while the PTIME algorithm solves many sub-problems in isolation. To further improve RankHow's scalability, we propose a novel approximation technique called symbolic gradient descent (Sym-GD). It exploits problem structure to more quickly find local minima of the error function. Experiments demonstrate that RankHow can solve realistic problems, finding more accurate linear scoring functions than the state of the art.

cs.DB↗

arXiv2023

Verification of GossipSub in ACL2s

GossipSub is a popular new peer-to-peer network protocol designed to disseminate messages quickly and efficiently by allowing peers to forward the full content of messages only to a dynamically selected subset of their neighboring peers (mesh neighbors) while gossiping about messages they have seen with the rest. Peers decide which of their neighbors to graft or prune from their mesh locally and periodically using a score for each neighbor. Scores are calculated using a score function that depends on mesh-specific parameters, weights and counters relating to a peer's performance in the network. Since a GossipSub network's performance ultimately depends on the performance of its peers, an important question arises: Is the score calculation mechanism effective in weeding out non-performing or even intentionally misbehaving peers from meshes? We answered this question in the negative in our companion paper by reasoning about GossipSub using our formal, official and executable ACL2s model. Based on our findings, we synthesized and simulated attacks against GossipSub which were confirmed by the developers of GossipSub, FileCoin, and Eth2.0, and publicly disclosed in MITRE CVE-2022-47547. In this paper, we present a detailed description of our model. We discuss design decisions, security properties of GossipSub, reasoning about the security properties in context of our model, attack generation and lessons we learnt when writing it.

cs.LO↗

arXiv2023

Proving Calculational Proofs Correct

Teaching proofs is a crucial component of any undergraduate-level program that covers formal reasoning. We have developed a calculational reasoning format and refined it over several years of teaching a freshman-level course, "Logic and Computation", to thousands of undergraduate students. In our companion paper, we presented our calculational proof format, gave an overview of the calculational proof checker (CPC) tool that we developed to help users write and validate proofs, described some of the technical and implementation details of CPC and provided several publicly available proofs written using our format. In this paper, we dive deeper into the implementation details of CPC, highlighting how proof validation works, which helps us argue that our proof checking process is sound.

cs.LO↗

arXiv2023

A Case Study in Analytic Protocol Analysis in ACL2

When verifying computer systems we sometimes want to study their asymptotic behaviors, i.e., how they behave in the long run. In such cases, we need real analysis, the area of mathematics that deals with limits and the foundations of calculus. In a prior work, we used real analysis in ACL2s to study the asymptotic behavior of the RTO computation, commonly used in congestion control algorithms across the Internet. One key component in our RTO computation analysis was proving in ACL2s that for all alpha in [0, 1), the limit as n approaches infinity of alpha raised to n is zero. Whereas the most obvious proof strategy involves the logarithm, whose codomain includes irrationals, by default ACL2 only supports rationals, which forced us to take a non-standard approach. In this paper, we explore different approaches to proving the above result in ACL2(r) and ACL2s, from the perspective of a relatively new user to each. We also contextualize the theorem by showing how it allowed us to prove important asymptotic properties of the RTO computation. Finally, we discuss tradeoffs between the various proof strategies and directions for future research.

cs.LO↗

arXiv2023

Using Counterexample Generation and Theory Exploration to Suggest Missing Hypotheses

Newcomers to ACL2 are sometimes surprised that ACL2 rejects formulas that they believe should be theorems, such as (REVERSE (REVERSE X)) = X. Experienced ACL2 users will recognize that the theorem only holds for intended values of X, and given ACL2's total logic, there are many counterexamples for which this formula is simply not true. Counterexample generation (cgen) is a technique that helps by giving the user a number of counterexamples (and also witnesses) to the formula, e.g., letting the user know that the intended theorem is false when X is equal to 10. In this paper we describe a tool called DrLA that goes further by suggesting additional hypotheses that will make the theorem true. In this case, for example, DrLA may suggest that X needs to be either a TRUE-LIST or a STRING. The suggestions are discovered using the ideas of theory exploration and subsumption from automated theorem proving.

cs.LO↗

arXiv2023

Calculational Proofs in ACL2s

Teaching college students how to write rigorous proofs is a critical objective in courses that introduce formal reasoning. Over the course of several years, we have developed a mechanically-checkable style of calculational reasoning that we used to teach over a thousand freshman-level undergraduate students how to reason about computation in our "Logic and Computation" class at Northeastern University. We were inspired by Dijkstra, who advocated the use of calculational proofs, writing "calculational proofs are almost always more effective than all informal alternatives, ..., the design of calculational proofs seems much more teachable than the elusive art of discovering an informal proof." Our calculational proof checker is integrated into ACL2s and is available as an Eclipse IDE plugin, via a Web interface, and as a stand-alone tool. It automatically checks proofs for correctness and provides useful feedback. We describe the architecture of the checker, its proof format, its underlying algorithms, its correctness and provide examples using proofs from our undergraduate class and from Dijkstra. We also describe our experiences using the proof checker to teach undergraduates how to formally reason about computation.

cs.LO↗

arXiv2023

Automated Grading of Automata with ACL2s

Almost all Computer Science programs require students to take a course on the Theory of Computation (ToC) which covers various models of computation such as finite automata, push-down automata and Turing machines. ToC courses tend to give assignments that require paper-and-pencil solutions. Grading such assignments takes time, so students typically receive feedback for their solutions more than a week after they complete them. We present the Automatic Automata Checker (A2C), an open source library that enables one to construct executable automata using definitions that mimic those found in standard textbooks. Such constructions are easy to reason about using semantic equivalence checks, properties and test cases. Instructors can conveniently specify solutions in the form of their own constructions. A2C can check for semantic equivalence between student and instructor solutions and can immediately generate actionable feedback, which helps students better understand the material. A2C can be downloaded and used locally by students as well as integrated into Learning Management Systems (LMS) like Gradescope to automatically grade student submissions and generate feedback. A2C is based on the ACL2s interactive theorem prover, which provides advanced methods for stating, proving and disproving properties. Since feedback is automatic, A2C can be deployed at scale and integrated into massively open online courses.

cs.LO↗

arXiv2022

ACL2s Systems Programming

ACL2 provides a systems programming capability that allows one to write code that uses and extends ACL2 inside of ACL2. However, for soundness reasons, ACL2 bars the unrestricted use of certain kinds of programming constructs, like destructive updates, higher-order functions, eval, and arbitrary macros. We devised a methodology for writing code in Common Lisp that allows one to access ACL2, ACL2s, and Common Lisp functionality in a unified way. We arrived at this methodology in the process of developing the ACL2 Sedan (ACL2s) and using it as a key component in formal-methods-enabled projects relating to gamified verification, education, proof checking, interfacing with external theorem provers and security. The methodology includes a library for performing ACL2 queries from Common Lisp, as well as guidelines and utilities that help address common needs. We call this methodology "ACL2s systems programming," to distinguish it from ACL2 systems programming. We show how our methodology makes it possible to easily develop tools that interface with ACL2 and ACL2s, and describe our experience using it in our research.

cs.LO↗

arXiv2021

A Reasoning Engine for the Gamification of Loop-Invariant Discovery

We describe the design and implementation of a reasoning engine that facilitates the gamification of loop-invariant discovery. Our reasoning engine enables students, computational agents and regular software engineers with no formal methods expertise to collaboratively prove interesting theorems about simple programs using browser-based, online games. Within an hour, players are able to specify and verify properties of programs that are beyond the capabilities of fully-automated tools. The hour limit includes the time for setting up the system, completing a short tutorial explaining game play and reasoning about simple imperative programs. Players are never required to understand formal proofs; they only provide insights by proposing invariants. The reasoning engine is responsible for managing and evaluating the proposed invariants, as well as generating actionable feedback.

cs.AI↗

arXiv2020

Introduction to Rank-polymorphic Programming in Remora (Draft)

Remora is a higher-order, rank-polymorphic array-processing programming language, in the same general class of languages as APL and J. It is intended for writing programs to be executed on parallel hardware. We provide an example-driven introduction to the language, and its general computational model, originally developed by Iverson for APL. We begin with Dynamic Remora, a variant of the language with a dynamic type system (as in Scheme or Lisp), to introduce the fundamental computational mechanisms of the language, then shift to Explicitly Typed Remora, a variant of the language with a static, dependent type system that permits the shape of the arrays being computed to be captured at compile time. This article can be considered an introduction to the general topic of the rank-polymorphic array-processing computational model, above and beyond the specific details of the Remora language. We do not address the details of type inference in Remora, that is, the assignment of explicit types to programs written without such annotations; this is ongoing research.

cs.PL↗

arXiv2019

The Semantics of Rank Polymorphism

Iverson's APL and its descendants (such as J, K and FISh) are examples of the family of "rank-polymorphic" programming languages. The principal control mechanism of such languages is the general lifting of functions that operate on arrays of rank (or dimension) $r$ to operate on arrays of any higher rank $r' > r$. We present a core, functional language, Remora, that captures this mechanism, and develop both a formal, dynamic semantics for the language, and an accompanying static, rank-polymorphic type system for the language. Critically, the static semantics captures the shape-based lifting mechanism of the language. We establish the usual progress and preservation properties for the type system, showing that it is sound, which means that "array shape" errors cannot occur at run time in a well-typed program. Our type system uses dependent types, including an existential type abstraction which permits programs to operate on arrays whose shape or rank is computed dynamically; however, it is restricted enough to permit static type checking. The rank-polymorphic computational paradigm is unusual in that the types of arguments affect the dynamic execution of the program -- they are what drive the rank-polymorphic distribution of a function across arrays of higher rank. To highlight this property, we additionally present a dynamic semantics for a partially erased variant of the fully-typed language and show that a computation performed with a fully-typed term stays in lock step with the computation performed with its partially erased term. The residual types thus precisely characterise the type information that is needed by the dynamic semantics, a property useful for the (eventual) construction of efficient compilers for rank-polymorphic languages.

cs.PL↗

arXiv2017

Partial Quantifier Elimination

We consider the problem of Partial Quantifier Elimination (PQE). Given formula exists(X)[F(X,Y) & G(X,Y)], where F, G are in conjunctive normal form, the PQE problem is to find a formula F*(Y) such that F* & exists(X)[G] is logically equivalent to exists(X)[F & G]. We solve the PQE problem by generating and adding to F clauses over the free variables that make the clauses of F with quantified variables redundant. The traditional Quantifier Elimination problem (QE) is a special case of PQE where G is empty so all clauses of the input formula with quantified variables need to be made redundant. The importance of PQE is twofold. First, many problems are more naturally formulated in terms of PQE rather than QE. Second, in many cases PQE can be solved more efficiently than QE. We describe a PQE algorithm based on the machinery of dependency sequents and give experimental results showing the promise of PQE.

cs.LO↗

arXiv2017

An Efficient Runtime Validation Framework based on the Theory of Refinement

We introduce a new methodology based on refinement for testing the functional correctness of hardware and low-level software. Our methodology overcomes several major drawbacks of the de facto testing methodologies used in industry: (1) it is difficult to determine completeness of the properties and tests under consideration (2) defining oracles for tests is expensive and error-prone (3) properties are defined in terms of low-level designs. Our approach compiles a formal refinement conjecture into a runtime check that is performed during simulation. We describe our methodology, discuss algorithmic issues, and provide experimental validation using a 5-stage RISCV pipelined microprocessor and hypervisor.

cs.LO↗