bluuebunny/crossref_metadata_2025_split huggingface dataset:
Tighter Construction of Tight Büchi Automata
Authors: Jankola Marek , Strejček Jan 
Published: April 2024

AbstractTight automata are useful in providing the shortest counterexample in LTL model checking and also in constructing a maximally satisfying strategy in LTL strategy synthesis. There exists a translation of LTL formulas to tight Büchi automata and several translations of Büchi automata to equivalent tight Büchi automata. This paper presents another translation of Büchi automata to equivalent tight Büchi automata. The translation is designed to produce smaller tight automata and it asymptotically improves the best-known upper bound on the size of a tight Büchi automaton equivalent to a given Büchi automaton. We also provide a lower bound, which is more precise than the previously known one. Further, we show that automata reduction methods based on quotienting preserve tightness. Our translation was implemented in a tool called Tightener. Experimental evaluation shows that Tightener usually produces smaller tight automata than the translation from LTL to tight automata known as CGH.
Synthesis with Privacy Against an Observer
Authors: Kupferman Orna , Leshkowitz Ofer , Shamash Halevy Naama 
Published: April 2024

AbstractWe study automaticsynthesisof systems that interact with their environment and maintainprivacyagainst an observer to the interaction. The system and the environment interact via setsIandOof input and output signals. The input to the synthesis problem contains, in addition to a specification, also a list ofsecrets, a function$$\textsf{cost}: I \cup O \rightarrow {\mathbb N}$$cost:I∪O→N, which maps each signal to the cost of hiding it, and a bound$$b \in {\mathbb N}$$b∈Non the budget that the system may use for hiding of signals. The desired output is an (I/O)-transducer$$\mathcal {T}$$Tand a set$$\mathcal {H} \subseteq I \cup O$$H⊆I∪Oof signals that respects the bound on the budget, thus$$\sum _{s \in \mathcal {H}} \textsf{cost}(s) \le b$$∑s∈Hcost(s)≤b, such that for every possible interaction of$$\mathcal {T}$$T, the generated computation satisfies the specification, yet an observer from which the signals in$$\mathcal {H}$$Hare hidden, cannot evaluate the secrets.We first show that the complexity of the problem is 2EXPTIME-complete for specifications and secrets in LTL, thus it is not harder than synthesis with no privacy requirements. We then analyze the complexity of the problem more carefully, isolating the two aspects that do not exist in traditional synthesis, namely the need to hide the value of the secrets and the need to choose the set$$\mathcal {H}$$H. We do this by studying settings in which traditional synthesis can be solved in polynomial time – when the specification formalism is deterministic automata and when the system is closed, and show that each of the two aspects involves an exponential blow-up in the complexity. We continue and studybounded synthesis with privacy, where the input also includes a bound on the size of the synthesized transducer, as well as a variant of the problem in which the observer hasknowledge about the specification, which can be helpful in evaluating the secrets. We study the effect of both variants on the different aspects of the problem and provide algorithms with a tight complexity.
Symbolic Solution of Emerson-Lei Games for Reactive Synthesis
Authors: Hausmann Daniel , Lehaut Mathieu , Piterman Nir 
Published: April 2024

AbstractEmerson-Lei conditions have recently attracted attention due to both their succinctness and their favorable closure properties. In the current work, we show how infinite-duration games with Emerson-Lei objectives can be analyzed in two different ways. First, we show that the Zielonka tree of the Emerson-Lei condition naturally gives rise to a new reduction to parity games. This reduction, however, does not result in optimal analysis. Second, we show based on the first reduction (and the Zielonka tree) how to provide a direct fixpoint-based characterization of the winning region. The fixpoint-based characterization allows for symbolic analysis. It generalizes the solutions of games with known winning conditions such as Büchi, GR[1], parity, Streett, Rabin and Muller objectives, and in the case of these conditions reproduces previously known symbolic algorithms and complexity results.We also show how the capabilities of the proposed algorithm can be exploited in reactive synthesis, suggesting a new expressive fragment of LTL that can be handled symbolically. Our fragment combines a safety specification and a liveness part. The safety part is unrestricted and the liveness part allows to define Emerson-Lei conditions on occurrences of letters. The symbolic treatment is enabled due to the simplicity of determinization in the case of safety languages and by using our new algorithm for game solving. This approach maximizes the number of steps solved symbolically in order to maximize the potential for efficient symbolic implementations.
Drawing from an Urn is Isometric
Authors: Jacobs Bart 
Published: April 2024

AbstractDrawing (a multiset of) coloured balls from an urn is one of the most basic models in discrete probability theory. Three modes of drawing are commonly distinguished: multinomial (draw-replace), hypergeometric (draw-delete), and Pólya (draw-add). These drawing operations are represented as maps from urns to distributions over multisets of draws. The set of urns is a metric space via the Wasserstein distance. The set of distributions over draws is also a metric space, using Wasserstein-over-Wasserstein. The main result of this paper is that the three draw operations are all isometries, that is, they preserve the Wasserstein distances.
Enriching Diagrams with Algebraic Operations
Authors: Villoria Alejandro , Basold Henning , Laarman Alfons 
Published: April 2024

AbstractIn this paper, we extend diagrammatic reasoning in monoidal categories with algebraic operations and equations. We achieve this by considering monoidal categories that are enriched in the category of Eilenberg-Moore algebras for a monad. Under the condition that this monad is monoidal and there is an adjunction between the free algebra functor and the underlying category functor, we construct an adjunction between symmetric monoidal categories and symmetric monoidal categories enriched over algebras for the monad. This allows us to devise an extension, and its semantics, of the ZX-calculus with probabilistic choices by freely enriching over convex algebras, which are the algebras of the finite distribution monad. We show how this construction can be used for diagrammatic reasoning of noise in quantum systems.
JPF: From 2003 to 2023
Authors: Artho Cyrille , Parízek Pavel , Qu Daohan , Galgali Varadraj , Yi Pu 
Published: April 2024

AbstractWe give an account of JPF’s current architecture as it has evolved over the last 20 years. Key changes include a modular, extensible design, and Java 11 support.Java 11 brought with it fundamental changes in the language and its runtime, in particular, a new modular library system, different compilation of string expressions to bootstrap methods, and changes in many internal interfaces that allow access to the loaded code and the virtual machine state. These changes required numerous adaptations in JPF to ensure a successful compilation and correct behavior under Java 11.
Automated Software Verification of Hyperliveness
Authors: Beutner Raven 
Published: April 2024

AbstractHyperproperties relate multiple executions of a program and are commonly used to specify security and information-flow policies. Most existing work has focused on the verification ofk-safety properties, i.e., properties that state that allk-tuples of execution traces satisfy a given property. In this paper, we study the automated verification of richer properties that combine universal and existential quantification over executions. Concretely, we consider$$\forall ^k\exists ^l$$∀k∃lproperties, which state that for allkexecutions, there existlexecutions that, together, satisfy a property. This captures important non-k-safety requirements, including hyperliveness properties such as generalized non-interference, opacity, refinement, and robustness. We design an automated constraint-based algorithm for the verification of$$\forall ^k\exists ^l$$∀k∃lproperties. Our algorithm leverages a sound-and-complete program logic and a (parameterized) strongest postcondition computation. We implement our algorithm in a tool called and report on encouraging experimental results.
Hitching a Ride to a Lasso: Massively Parallel On-The-Fly LTL Model Checking
Authors: Osama Muhammad , Wijs Anton 
Published: April 2024

AbstractThe need for massively parallel algorithms, suitable to exploit the computational power of hardware such as graphics processing units, is ever increasing. In this paper, we propose a new algorithm for the on-the-fly verification of Linear-Time Temporal Logic (LTL) formulae [45] that is aimed at running on such devices. We prove its correctness and termination guarantee, and experimentally compare a GPU implementation with state-of-the-art LTL model checkers. Our new GPU LTL-checking algorithm is up to 150$$\times $$
×
faster on proving the correctness of a system than LTSmin running on a 32-core high-end CPU, and is more economic in using the available memory.
Weakest Precondition Inference for Non-Deterministic Linear Array Programs
Authors: Sumanth Prabhu S. , D’Souza Deepak , Chakraborty Supratik , Venkatesh R , Fedyukovich Grigory 
Published: April 2024

AbstractPrecondition inferenceis an important problem with many applications. Existing precondition inference techniques for programs with arrays have limited ability to find and prove the weakest preconditions, especially when programs have non-determinism. In this paper, we propose an approach to overcome the limitation. As the problem is uncomputable in general, our approach targets a special class of programs called linear array programs that are commonly encountered in practical applications and have been studied before. We also focus on a class of quantified formulas for pre- and postconditions that suffice to specify program properties in many applications. Our approach uses two novel techniques calledStructural Array Abduction(SAA) andSpecialized Maximality Checking(SMC). SAA is an abduction-based technique used to infer quantified preconditions and necessary inductive invariants. SMC proves that an inferred precondition is the weakest by finding an under-approximated program and solving the complement verification problem on it using SAA. When inconclusive, it attempts to weaken the precondition. Our approach can infer (and also prove) the weakest preconditions for a range of benchmarks relatively quickly, and outperforms competing techniques.
Training for Verification: Increasing Neuron Stability to Scale DNN Verification
Authors: Xu Dong , Mozumder Nusrat Jahan , Duong Hai , Dwyer Matthew B. 
Published: April 2024

AbstractWith the growing use of deep neural networks(DNN) in mission and safety-critical applications, there is an increasing interest in DNN verification. Unfortunately, increasingly complex network structures, non-linear behavior, and high-dimensional input spaces combine to make DNN verification computationally challenging. Despite tremendous advances, DNN verifiers are still challenged to scale to large verification problems. In this work, we explore how the number of stable neurons under the precondition of a specification gives rise to verification complexity. We examine prior work on the problem, adapt it, and develop several novel approaches to increase stability. We demonstrate that neuron stability can be increased substantially without compromising model accuracy and this yields a multi-fold improvement in DNN verifier performance.
SWAT: Modular Dynamic Symbolic Execution for Java Applications using Dynamic Instrumentation (Competition Contribution)
Authors: Loose Nils , Mächtle Felix , Sieck Florian , Eisenbarth Thomas 
Published: April 2024

AbstractSWAT is a novel dynamic symbolic execution engine for Java applications utilizing dynamic instrumentation. SWAT’s unique modular design facilitates flexible communication between its symbolic explorer and executor using HTTP endpoints, thus enhancing adaptability to diverse application scenarios. The symbolic executor’s ability to attach to Java applications enables efficient constraint generation and path exploration. SWAT employs JavaSMT for constraint generation and ASM for bytecode instrumentation, ensuring robust performance. SWAT’s efficacy is evaluated in the Java Track of SV-COMP 2024, achieving fourth place.
Theta: Abstraction Based Techniques for Verifying Concurrency (Competition Contribution)
Authors: Bajczi Levente , Telbisz Csanád , Somorjai Márk , Ádám Zsófia , Dobos-Kovács Mihály , Szekeres Dániel , Mondok Milán , Molnár Vince 
Published: April 2024

AbstractThetais a model checking framework, with a strong emphasis on effectively handling concurrency in software using abstraction refinement algorithms. In SV-COMP 2024, we use 1) an abstraction-aware partial order reduction; 2) a dynamic statement reduction technique; and 3) enhanced support for call stacks to handle recursive programs. We integrate these techniques in an improved architecture with inherent support for portfolio-based verification using dynamic algorithm selection, with a diverse selection of supported SMT solvers as well. In this paper we detail the advances ofThetaregarding concurrent and recursive software support.
Trocq: Proof Transfer for Free, With or Without Univalence
Authors: Cohen Cyril , Crance Enzo , Mahboubi Assia 
Published: April 2024

AbstractThis article presents Trocq, a new proof transfer framework for dependent type theory. Trocq is based on a novel formulation of type equivalence, used to generalize the univalent parametricity translation. This framework takes care of avoiding dependency on the axiom of univalence when possible, and may be used with more relations than just equivalences. We have implemented a corresponding plugin for the interactive theorem prover, in the meta-language.
Monadic Intersection Types, Relationally
Authors: Gavazzo Francesco , Treglia Riccardo , Vanoni Gabriele 
Published: April 2024

AbstractWe extend intersection types to a computational $$\lambda $$
λ
-calculus with algebraic operations à la Plotkin and Power. We achieve this by considering monadic intersections—whereby computational effects appear not only in the operational semantics, but also in the type system. Since in the effectful setting termination is not anymore the only property of interest, we want to analyze the interactive behavior of typed programs with the environment. Indeed, our type system is able to characterize the natural notion of observation, both in the finite and in the infinitary setting, and for a wide class of effects, such as output, cost, pure and probabilistic nondeterminism, and combinations thereof. The main technical tool is a novel combination of syntactic techniques with abstract relational reasoning, which allows us to lift all the required notions, e.g. of typability and logical relation, to the monadic setting.
Circuit Width Estimation via Effect Typing and Linear Dependency
Authors: Colledan Andrea , Dal Lago Ugo 
Published: April 2024

AbstractCircuit description languages are a class of quantum programming languages in which programs are classical and produce a description of a quantum computation, in the form of a quantum circuit. Since these programs can leverage all the expressive power of high-level classical languages, circuit description languages have been successfully used to describe complex and practical quantum algorithms, whose circuits, however, may involve many more qubits and gate applications than current quantum architectures can actually muster. In this paper, we present , a circuit description language endowed with a linear dependent type-and-effect system capable of deriving parametric upper bounds on the width of the circuits produced by a program. We prove both the standard type safety results and that the resulting resource analysis is correct with respect to a big-step operational semantics. We also show that our approach is expressive enough to verify realistic quantum algorithms.
Verified Inlining and Specialisation for PureCake
Authors: Kanabar Hrutvik , Korban Kacper , Myreen Magnus O. 
Published: April 2024

AbstractInlining is a crucial optimisation when compiling functional programming languages. This paper describes how we have implemented and verified function inlining and loop specialisation for PureCake, a verified compiler for a Haskell-like (purely functional, lazy) programming language. A novel aspect of our formalisation is that we justify inlining by pushing and pulling "Image missing"-bindings. All of our work has been mechanised in the HOL4 interactive theorem prover.
“If You Really Want to Change the World, the Smartest Way to do so is Through Education”
Authors: Ehlers Ulf-Daniel , Eigbrecht Laura 
Published: April 2024

AbstractAngela Duckworth (Fig. 10.1) is the Rosa Lee and Egbert Chang Professor of Psychology at the University of Pennsylvania and the founder of Character Lab, a nonprofit that advances scientific insights to help kids thrive. Before her research career, Angela Duckworth was a math and science teacher at public schools, founding her passion for education. With one of the most-viewed TED talks of all time and the bestselling book Grit: The Power of Passion and Perseverance as well as as a podcast host, Angela Duckworth shares her research to a broader audience. In this conversation, we discuss the concepts of Future Skills and character strengths and what they can contribute to shape the future of education.
Towards a Future Skills Framework for Higher Education
Authors: Ehlers Ulf-Daniel 
Published: April 2024

AbstractSkills are the ability and capacity to act and be able to use one’s knowledge in a responsible way to achieve a goal. Future Skills are an emerging concept based on the theory of competence and action, which form a holistic concept, involving the mobilization of knowledge, skills, attitudes, and values to meet complex demands. The NextSkills study distinguishes between three different types of skills: learning and growth skills which refer to an individual’s development process, design and innovation skills which refer to an individual’s capacity to deal with a certain object, task, or assignment in a new, creative way, and co-creation skills which refer to an individual’s way to productively shape their social environment and relation to the world.
Formative Assessment of 21st Century Skills
Authors: Seidl Tobias 
Published: April 2024

AbstractSince 2016, the Faculty of Information and Communication at Stuttgart Media University has integrated comprehensive key competence modules in all its BA study programs. The aim is to prepare students for a demanding study program as well as an uncertain and therefore challenging future. Part of the modules is a sophisticated formative assessment approach, which supports the individual learning journey of the students. This chapter describes the design of the modules, as well as the assessment setting, in detail. The good practice example encourages reflection on one’s own approaches and perspective to teaching and assessing 21st Century Skills.
Future Higher Education in New Zealand: Creating a Universal Learning Community for Future Skills
Authors: Marshall Stephen 
Published: April 2024

AbstractSkills challenges for the future embody major challenges for a national system of education. One is the ability of skills-development mechanisms to scale well beyond the limits of the existing models while also reducing dramatically the associated costs of development and operation for providers, and the costs of participation and achievement demonstration for learners. A second is that of being responsive to a rapidly changing environment, evolving existing structures to meet new needs. This chapter explores the New Zealand context for these challenges. A future-facing model, responding to these challenges and using inspiration from the New Zealand Māori concept of ‘Ako’, is presented. Described as ‘microlearning’, this model is proposed as an alternative for Future Skills development that avoids the pitfalls of credentialised approaches. The potential for microlearning for Future Skills development in regulated professionals is suggested as a starting point for initial exploration of this new model.
iRhom2 regulates ectodomain shedding and surface expression of the major histocompatibility complex (MHC) class I
Authors: Calligaris Matteo , Spanò Donatella P. , Bonelli Simone , Müller Stephan A. , Carcione Claudia , D’apolito Danilo , Amico Giandomenico , Miele Monica , Di Bella Mariangela , Zito Giovanni , Nuti Elisa , Rossello Armando , Blobel Carl P. , Lichtenthaler Stefan F. , Scilabra Simone D. 
Published: April 2024

AbstractProteolytic release of transmembrane proteins from the cell surface, the so called ectodomain shedding, is a key process in inflammation. Inactive rhomboid 2 (iRhom2) plays a crucial role in this context, in that it guides maturation and function of the sheddase ADAM17 (a disintegrin and metalloproteinase 17) in immune cells, and, ultimately, its ability to release inflammatory mediators such as tumor necrosis factor α (TNFα). Yet, the macrophage sheddome of iRhom2/ADAM17, which is the collection of substrates that are released by the proteolytic complex, is only partly known. In this study, we applied high-resolution proteomics to murine and human iRhom2-deficient macrophages for a systematic identification of substrates, and therefore functions, of the iRhom2/ADAM17 proteolytic complex. We found that iRhom2 loss suppressed the release of a group of transmembrane proteins, including known (e.g. CSF1R) and putative novel ADAM17 substrates. In the latter group, shedding of major histocompatibility complex class I molecules (MHC-I) was consistently reduced in both murine and human macrophages when iRhom2 was ablated. Intriguingly, it emerged that in addition to its shedding, iRhom2 could also control surface expression of MHC-I by an undefined mechanism. We have demonstrated the biological significance of this process by using an in vitro model of CD8+ T-cell (CTL) activation. In this model, iRhom2 loss and consequent reduction of MHC-I expression on the cell surface of an Epstein-Barr virus (EBV)-transformed lymphoblastoid cell line dampened activation of autologous CTLs and their cell-mediated cytotoxicity. Taken together, this study uncovers a new role for iRhom2 in controlling cell surface levels of MHC-I by a dual mechanism that involves regulation of their surface expression and ectodomain shedding.
Bitcoin as a Transaction Ledger: A Composable Treatment
Authors: Badertscher Christian , Maurer Ueli , Tschudi Daniel , Zikas Vassilis 
Published: April 2024

AbstractBitcoin is one of the most prominent examples of a distributed cryptographic protocol that is extensively used in reality. Nonetheless, existing security proofs are property-based, and as such they do not support composition. In this work, we put forth a universally composable treatment of the Bitcoin protocol. We specify the goal that Bitcoin aims to achieve as an instance of a parameterizable ledger functionality and present a UC abstraction of the Bitcoin blockchain protocol. Our ideal functionality is weaker than the first proposed candidate by Kiayias, Zhou, and Zikas [EUROCRYPT’16], but unlike the latter suggestion, which is arguably not implementable by the UC Bitcoin protocol, we prove that the one proposed here is securely UC-realized by the protocol assuming access to a global clock, to model time-based executions, a random oracle, to model hash functions, and an idealized network, to model message dissemination. We further show how known property-based approaches can be cast as special instances of our treatment and how their underlying assumptions can be cast in UC as part of the setup functionalities and without restricting the environment or the adversary.