bluuebunny/crossref_metadata_2025_split huggingface dataset:
CPV: A Circuit-Based Program Verifier
Authors: Chien Po-Chun , Lee Nian-Ze 
Published: April 2024

AbstractWe submit to SV-COMP 2024CPV, a circuit-based software verifier for C programs.CPVutilizes sequential circuits as its intermediate representation and invokes hardware model checkers to analyze the reachability safety of C programs. As the frontend, it usesKratos2, a recently proposed verification tool, to translate a C program to a sequential circuit. As the backend, state-of-the-art hardware model checkersABCandAVRare employed to verify the translated circuits. We configure the hardware model checkers to run various analyses, including IC3/PDR, interpolation-based model checking, and$$k$$k-induction. Information discovered by hardware model checkers is represented as verification witnesses. In the competition,CPVachieved comparable performance against participants whose intermediate representations are based on control-flow graphs. In the categoryReachSafety, it outperformed several mature software verifiers as a first-year participant.CPVmanifests the feasibility of sequential circuits as an alternative intermediate representation for program analysis and enables head-to-head algorithmic comparison between hardware and software verification.
PROTON: PRObes for Termination Or Not (Competition Contribution)
Authors: Metta Ravindra , Karmarkar Hrishikesh , Madhukar Kumar , Venkatesh R. , Chakraborty Supratik 
Published: April 2024

AbstractPROTON is a tool to check whether a given C program has a non-terminating behaviour or not. It is built around the C Bounded Model Checker (CBMC). CBMC cannot prove non-termination directly, as all non-terminating runs are unbounded. PROTON annotates the loops in a given program with assertions that check for a recurrent program state. Violation of such an assertion shows the existence of a recurrent state and thereby proves non-termination. PROTON also transforms the violating trace returned by CBMC into a non-termination witness for the program.
Gray-Box Fuzzing via Gradient Descent and Boolean Expression Coverage
Authors: Jonáš Martin , Strejček Jan , Trtík Marek , Urban Lukáš 
Published: April 2024

AbstractWe present a gray-box fuzzing approach based on several new ideas. While standard gray-box fuzzing aims to cover all branches of the input program, our approach primarily aims to cover both results of each Boolean expression. To achieve this goal, we track the distances to flipping these results and we dynamically detect the input bytes that influence the distance. Then we use this information to efficiently flip the results. More precisely, we apply gradient descent on the detected bytes or we create new inputs by using detected bytes from different inputs.We implemented our approach in a tool called Fizzer. An evaluation on the benchmarks of Test-Comp 2023 shows that Fizzer is fully competitive with the winning tools of the competition, which use advanced formal methods like symbolic execution or bounded model checking, usually in combination with fuzzing.
Fast Symbolic Computation of Bottom SCCs
Authors: Jakobsen Anna Blume , Jørgensen Rasmus Skibdahl Melanchton , van de Pol Jaco , Pavlogiannis Andreas 
Published: April 2024

AbstractThe computation of bottom strongly connected components (BSCCs) is a fundamental task in model checking, as well as in characterizing the attractors of dynamical systems. As such, symbolic algorithms for BSCCs have received special attention, and are based on the idea that the computation of an SCC can be stopped early, as soon as it is deemed to be non-bottom.In this paper we introduce $$\textsc {Pendant}$$

P

E
N
D
A
N
T

, a new symbolic algorithm for computing BSCCs which runs in linear symbolic time. In contrast to the standard approach of escaping non-bottom SCCs, $$\textsc {Pendant}$$

P

E
N
D
A
N
T

aims to start the computation from nodes that are likely to belong to BSCCs, and thus is more effective in sidestepping SCCs that are non-bottom. Moreover, we employ a simple yet powerful deadlock-detection technique, that quickly identifies singleton BSCCs before the main algorithm is run. Our experimental evaluation on three diverse datasets of 553 models demonstrates the efficacy of our two methods: $$\textsc {Pendant}$$

P

E
N
D
A
N
T

is decisively faster than the standard existing algorithm for BSCC computation, while deadlock detection improves the performance of each algorithm significantly.
Btor2-Cert: A Certifying Hardware-Verification Framework Using Software Analyzers
Authors: Ádám Zsófia , Beyer Dirk , Chien Po-Chun , Lee Nian-Ze , Sirrenberg Nils 
Published: April 2024

AbstractFormal verification is essential but challenging: Even the best verifiers may produce wrong verification verdicts.Certifyingverifiers enhance the confidence in verification results by generating awitnessfor other tools to validate the verdict independently. Recently, translating the hardware-modeling languageBtor2to software, such as the programming language C or LLVM intermediate representation, has been actively studied and facilitated verifying hardware designs by software analyzers. However, it remained unknown whether witnesses produced by software verifiers contain helpful information about the original circuits and how such information can aid hardware analysis. We propose a certifying and validating frameworkBtor2-Certto verify safety properties ofBtor2circuits, combiningBtor2-to-C translation, software verifiers, and a new witness validatorBtor2-Val, to answer the above open questions.Btor2-Certtranslates a softwareviolation witnessto aBtor2violation witness; As theBtor2language lacks a format forcorrectness witnesses, we encode invariants in software correctness witnesses asBtor2circuits. The validatorBtor2-Valchecks violation witnesses by circuit simulation and correctness witnesses byvalidation via verification. In our evaluation,Btor2-Certsuccessfully utilized software witnesses to improve quality assurance of hardware. By invoking the software verifierCbmcon translated programs, it uniquely solved, with confirmed witnesses, 8 % of the unsafe tasks for which the hardware verifierABCfailed to detect bugs.
Auction-Based Scheduling
Authors: Avni Guy , Mallik Kaushik , Sadhukhan Suman 
Published: April 2024

AbstractSequential decision-making tasks often require satisfaction of multiple, partially-contradictory objectives. Existing approaches are monolithic, where a singlepolicyfulfills all objectives. We presentauction-based scheduling, adecentralizedframework for multi-objective sequential decision making. Each objective is fulfilled using a separate and independent policy. Composition of policies is performed at runtime, where at each step, the policies simultaneously bid from pre-allocated budgets for the privilege of choosing the next action. The framework allows policies to be independently created, modified, and replaced. We study path planning problems on finite graphs with two temporal objectives and present algorithms to synthesize policies together with bidding policies in a decentralized manner. We consider three categories of decentralized synthesis problems, parameterized by the assumptions that the policies make on each other. We identify a class of assumptions calledassume-admissiblefor which synthesis is always possible for graphs whose every vertex has at most two outgoing edges.
Definitional Functoriality for Dependent (Sub)Types
Authors: Laurent Théo , Lennon-Bertrand Meven , Maillard Kenji 
Published: April 2024

AbstractDependently typed proof assistant rely crucially on definitional equality, which relates types and terms that are automatically identified in the underlying type theory. This paper extends type theory with definitional functor laws, equations satisfied propositionally by a large class of container-like type constructors $$F : {\text {Type}}\rightarrow {\text {Type}}$$

F
:
Type
→
Type

, equipped with a $$\textrm{map}_{F} {{\,\mathrm{:}\,}}(A \rightarrow B) \rightarrow F\,A \rightarrow F\,B$$

map
F

:

(
A
→
B
)

→
F

A
→
F

B

, such as lists or trees. Promoting these equations to definitional ones strengthens the theory, enabling slicker proofs and more automation for functorial type constructors. This extension is used to modularly justify a structural form of coercive subtyping, propagating subtyping through type formers in a map-like fashion. We show that the resulting notion of coercive subtyping, thanks to the extra definitional equations, is equivalent to a natural and implicit form of subsumptive subtyping. The key result of decidability of type-checking in a dependent type system with functor laws for lists has been entirely mechanized in Coq.
Layered Modal Type Theory
Authors: Hu Jason Z. S. , Pientka Brigitte 
Published: April 2024

AbstractWe introduce layering to modal type theory to combine type theory with intensional analysis. In particular, we demonstrate this idea by developing a 2-layered modal type theory. At the core of this type theory (layer 0) is a simply typed $$\lambda $$
λ
-calculus with no modality. Layer 1 is obtained by extending the core language with one layer of contextual $$\square $$
□
types to support pattern matching on potentially open code from layer 0 while retaining normalization. Although both layers fundamentally share the same language and the same typing judgment, we only allow computation at layer 1. As a consequence, layer 0 accurately captures the syntactic representation of code in contrast to the computational behaviors at layer 1. The system is justified by normalization by evaluation (NbE) using a presheaf model. The normalization algorithm extracted from the model is sound and complete and is implemented in Agda.Layered modal type theory provides a uniform foundation for meta-programming with intensional analysis. We see this work as an important step towards a foundational way to support meta-programming in proof assistants.
Program Synthesis from Graded Types
Authors: Hughes Jack , Orchard Dominic 
Published: April 2024

AbstractGraded type systems are a class of type system for fine-grained quantitative reasoning about data-flow in programs. Through the use of resource annotations (or grades), a programmer can express various program properties at the type level, reducing the number of typeable programs. These additional constraints on types lend themselves naturally to type-directed program synthesis, where this information can be exploited to constrain the search space of programs. We present a synthesis algorithm for a graded type system, where grades form an arbitrary pre-ordered semiring. Harnessing this grade information in synthesis is non-trivial, and we explore some of the issues involved in designing and implementing a resource-aware program synthesis tool. In our evaluation we show that by harnessing grades in synthesis, the majority of our benchmark programs (many of which involve recursive functions over recursive ADTs) require less exploration of the synthesis search space than a purely type-driven approach and with fewer needed input-output examples. This type-and-graded-directed approach is demonstrated for the research language Granule but we also adapt it for synthesising Haskell programs that use GHC’s linear types extension.
A Formal Treatment of Bidirectional Typing
Authors: Chen Liang-Ting , Ko Hsiang-Shang 
Published: April 2024

AbstractThere has been much progress in designing bidirectional type systems and associated type synthesis algorithms, but mainly on a case-by-case basis. To remedy the situation, this paper develops a general and formal theory of bidirectional typing for simply typed languages: for every signature that specifies a mode-correct bidirectionally typed language, there exists a proof-relevant type synthesiser which, given an input abstract syntax tree, constructs a typing derivation if any, gives its refutation if not, or reports that the input does not have enough type annotations. Sufficient conditions for deriving a type synthesiser such as soundness, completeness, and mode-correctness are studied universally for all signatures. We propose a preprocessing step called mode decoration, which helps the user to deal with missing type annotations. The entire theory is formally implemented in Agda, so we provide a verified generator of proof-relevant type synthesisers as a by-product of our formalism.
Generic bidirectional typing for dependent type theories
Authors: Felicissimo Thiago 
Published: April 2024

AbstractBidirectional typing is a discipline in which the typing judgment is decomposed explicitly into inference and checking modes, allowing to control the flow of type information in typing rules and to specify algorithmically how they should be used. Bidirectional typing has been fruitfully studied and bidirectional systems have been developed for many type theories. However, the formal development of bidirectional typing has until now been kept confined to specific theories, with general guidelines remaining informal. In this work, we give a generic account of bidirectional typing for a general class of dependent type theories. This is done by first giving a general definition of type theories (or equivalently, a logical framework), for which we define declarative and bidirectional type systems. We then show, in a theory-independent fashion, that the two systems are equivalent. This equivalence is then explored to establish the decidability of typing for weak normalizing theories, yielding a generic type-checking algorithm that has been implemented in a prototype and used in practice with many theories.
A Modular Soundness Theory for the Blackboard Analysis Architecture
Authors: Keidel Sven , Helm Dominik , Roth Tobias , Mezini Mira 
Published: April 2024

AbstractSound static analyses are an important ingredient for compiler optimizations and program verification tools. However, mathematically proving that a static analysis is sound is a difficult task due to two problems. First, soundness proofs relate two complicated program semantics (the static and the dynamic semantics) which are hard to reason about. Second, the more the static and dynamic semantics differ, the more work a soundness proof needs to do to bridge the impedance mismatch. These problems increase the effort and complexity of soundness proofs. Existing soundness theories address these problems by deriving both the dynamic and static semantics from the same artifact, often called generic interpreter. A generic interpreter provides a common structure along which a soundness proof can be composed, which avoids having to reason about the analysis as a whole. However, a generic interpreter restricts which analyses can be derived, as all derived analyses must roughly follow the program execution order.To lift this restriction, we develop a soundness theory for the blackboard analysis architecture, which is capable of describing backward, demand-driven, and summary-based analyses. The architecture describes static analyses with small independent modules, which communicate via a central store. Soundness of a compound analysis follows from soundness of all of its modules. Furthermore, modules can be proven sound independently, even though modules depend on each other. We evaluate our theory by proving soundness of four analyses: a pointer and call-graph analysis, a reflection analysis, an immutability analysis, and a demand-driven reaching definitions analysis.
Detection of Uncaught Exceptions in Functional Programs by Abstract Interpretation
Authors: Lermusiaux Pierre , Montagu Benoît 
Published: April 2024

AbstractException handling is a key feature in modern programming languages. Exceptions can be used to deal with errors, or as a means to control the flow of execution of a program. Since they might unexpectedly terminate a program, unhandled exceptions are a serious safety concern. We propose a static analysis to detect uncaught exceptions in functional programs, that is defined as an abstract interpreter. It computes a description of the values potentially returned by a program using a novel abstract domain, that can express inductively defined sets of values. Simultaneously, the analysis infers the possibly raised exceptions, by computing in theabstract exception monad. This abstract interpreter has been implemented as an effective static analyser for a large subset of programs, that supports mutable data types, the module system, and dynamically extensible data types such as the exception type. The analyser has been evaluated on several hundreds of programs.
On the Hardness of Analyzing Quantum Programs Quantitatively
Authors: Avanzini Martin , Moser Georg , Péchoux Romain , Perdrix Simon 
Published: April 2024

AbstractIn this paper, we study quantitative properties of quantum programs. Properties of interest include (positive) almost-sure termination, expected runtime or expected cost, that is, for example, the expected number of applications of a given quantum gate, etc. After studying the completeness of these problems in the arithmetical hierarchy over the Clifford+T fragment of quantum mechanics, we express these problems using a variation of a quantum pre-expectation transformer, a weakest pre-condition based technique that allows to symbolically compute these quantitative properties. Under a smooth restriction—a restriction to polynomials of bounded degree over a real closed field—we show that the quantitative problem, which consists in finding an upper-bound to the pre-expectation, can be decided in time double-exponential in the size of a program, thus providing, despite its great complexity, one of the first decidable results on the analysis and verification of quantum programs. Finally, we sketch how the latter can be transformed into an efficient synthesis method.
Reconciling Partial and Local Invertibility
Authors: Ågren Thuné Anders , Matsuda Kazutaka , Wang Meng 
Published: April 2024

AbstractInvertible programming languages specify transformations to be run in two directions, such as compression/decompression or encryption/decryption. Two key concepts in invertible programming languages are partial invertibility and local invertibility. Partial invertibility lets invertible code be parameterized by the results of non-invertible code, whereas local invertibility requires all code to be invertible. The former allows for more flexible programming, while the latter has connections to domains such as low-energy computing and quantum computing. We find that existing approaches lack a satisfying treatment of partial invertibility, leaving the connection to local invertibility unclear.In this paper, we identify four core constructs for partially invertible programming, and show how to give them a locally invertible interpretation. We show the expressiveness of the constructs by designing the functional invertible language Kalpis, and show how to give them a locally invertible semantics using the novel arrow combinator language $$\textsc {rrArr}$$

R
R

A

R
R

—the key idea is viewing partial invertibility as an invertible effect. By formalizing the two systems and giving Kalpis semantics by translation to $$\textsc {rrArr}$$

R
R

A

R
R

, we reconcile partial and local invertibility, solving an open problem in the field. All formal developments are mechanized in Agda.
A Denotational Approach to Release/Acquire Concurrency
Authors: Dvir Yotam , Kammar Ohad , Lahav Ori 
Published: April 2024

AbstractWe present a compositional denotational semantics for a functional language with first-class parallel composition and shared-memory operations whose operational semantics follows the Release/Acquire weak memory model (RA). The semantics is formulated in Moggi’s monadic approach, and is based on Brookes-style traces. To do so we adapt Brookes’s traces to Kang et al.’s view-based machine for RA, and supplement Brookes’s mumble and stutter closure operations with additional operations, specific to RA. The latter provides a more nuanced understanding of traces that uncouples them from operational interrupted executions. We show that our denotational semantics is adequate and use it to validate various program transformations of interest. This is the first work to put weak memory models on the same footing as many other programming effects in Moggi’s standard monadic approach.
Creating the University of the Future: A Global Panorama on Future Skills
Authors: Ehlers Ulf-Daniel , Eigbrecht Laura 
Published: April 2024

AbstractThe challenge of promoting Future Skills is one of the currently most debated ones for higher education institutions all over the world. In this chapter, the editors provide a conceptual basis for the contributed chapters as well as an overview of the sections and contributions of this book. The concept and relevance of Future Skills for Higher Education on a global scale is addressed, followed by an outline of how future universities could look like and which trends will shape this future. Followed by this, the five sections of the Creating the University of the Future book are introduced with short summaries of the chapters and the perspectives they contribute to discussing, promoting and reimagining Future Skills learning in higher education.
Learning Design for Future Skills Development in Small State Contexts
Authors: Gunness Sandhya , Ferreira-Meyers Karen , Daradoumis Thanasis 
Published: April 2024

AbstractThe small Southern African states of Mauritius and Eswatini, with respect to their high levels of digital literacy and telecommunications infrastructure, have great potential for meeting future challenges as regards capacity building and developing a globalized workforce. However, the weaknesses of a decoupled University-Industry R&D collaboration, low-level business sophistication, a lack of appropriate knowledge workers, and manifest skills mismatches could create a difficult future for university graduates in these two countries. Within an African context, and with heavy reliance on imported and globalized products and resources, there is a common need for building resilience, self-efficacy, intra- and entrepreneurial skills, emotional intelligence, and growth mindsets as essential competencies for our future “peopleware”, as opposed to hardware and software. This concept, made popular by Lister and DeMarco, in the context of increasing digitization, brings back the softer and more discerning human elements in times where algorithms are increasingly making decisions and influencing our behavior. This chapter presents an attempt to equip recently graduated young citizens with a set of transdisciplinary skills and competencies which can build the above-mentioned important attributes and values along with the depth of academic knowledge gained at the university. As small state developing countries with colonial backgrounds, our strong sense of community, togetherness, resilience, faith, and tolerance should permeate within our intellectual siege.