bluuebunny/crossref_metadata_2025_split huggingface dataset:
HOLL: Program Synthesis for Higher Order Logic Locking
Authors: Takhar Gourav , Karri Ramesh , Pilato Christian , Roy Subhajit 
Published: March 2022

AbstractLogic locking “hides” the functionality of a digital circuit to protect it from counterfeiting, piracy, and malicious design modifications. The original design is transformed into a “locked” design such that the circuit reveals its correct functionality only when it is “unlocked” with a secret sequence of bits—the key bit-string. However, strong attacks, especially the SAT attack that uses a SAT solver to recover the key bit-string, have been profoundly effective at breaking the locked circuit and recovering the circuit functionality.We lift logic locking to Higher Order Logic Locking (HOLL) by hiding a higher-order relation, instead of a key of independent values, challenging the attacker to discover this key relation to recreate the circuit functionality. Our technique uses program synthesis to construct the locked design and synthesize a corresponding key relation. HOLL has low overhead and existing attacks for logic locking do not apply as the entity to be recovered is no more a value. To evaluate our proposal, we propose a new attack (SynthAttack) that uses an inductive synthesis algorithm guided by an operational circuit as an input-output oracle to recover the hidden functionality. SynthAttack is inspired by the SAT attack, and similar to the SAT attack, it is verifiably correct, i.e., if the correct functionality is revealed, a verification check guarantees the same. Our empirical analysis shows that SynthAttack can break HOLL for small circuits and small key relations, but it is ineffective for real-life designs.
A New Approach for Active Automata Learning Based on Apartness
Authors: Vaandrager Frits , Garhewal Bharat , Rot Jurriaan , Wißmann Thorsten 
Published: March 2022

AbstractWe present $$L^{\#}$$

L
#

, a new and simple approach to active automata learning. Instead of focusing on equivalence of observations, like the $$L^{*}$$

L

∗

algorithm and its descendants, $$L^{\#}$$

L
#

takes a different perspective: it tries to establish apartness, a constructive form of inequality. $$L^{\#}$$

L
#

does not require auxiliary notions such as observation tables or discrimination trees, but operates directly on tree-shaped automata. $$L^{\#}$$

L
#

has the same asymptotic query and symbol complexities as the best existing learning algorithms, but we show that adaptive distinguishing sequences can be naturally integrated to boost the performance of $$L^{\#}$$

L
#

in practice. Experiments with a prototype implementation, written in Rust, suggest that $$L^{\#}$$

L
#

is competitive with existing algorithms.
Learning Realtime One-Counter Automata
Authors: Bruyère Véronique , Pérez Guillermo A. , Staquet Gaëtan 
Published: March 2022

AbstractWe present a new learning algorithm for realtime one-counter automata. Our algorithm uses membership and equivalence queries as in Angluin’s $${L}^*$$

L

∗

algorithm, as well as counter value queries and partial equivalence queries. In a partial equivalence query, we ask the teacher whether the language of a given finite-state automaton coincides with a counter-bounded subset of the target language. We evaluate an implementation of our algorithm on a number of random benchmarks and on a use case regarding efficient JSON-stream validation.
Scalable Anytime Algorithms for Learning Fragments of Linear Temporal Logic
Authors: Raha Ritam , Roy Rajarshi , Fijalkow Nathanaël , Neider Daniel 
Published: March 2022

AbstractLinear temporal logic (LTL) is a specification language for finite sequences (called traces) widely used in program verification, motion planning in robotics, process mining, and many other areas. We consider the problem of learning formulas in fragments of LTL without the $$\mathbf {U}$$
U
-operator for classifying traces; despite a growing interest of the research community, existing solutions suffer from two limitations: they do not scale beyond small formulas, and they may exhaust computational resources without returning any result. We introduce a new algorithm addressing both issues: our algorithm is able to construct formulas an order of magnitude larger than previous methods, and it is anytime, meaning that it in most cases successfully outputs a formula, albeit possibly not of minimal size. We evaluate the performances of our algorithm using an open source implementation against publicly available benchmarks.
NeuReach: Learning Reachability Functions from Simulations
Authors: Sun Dawei , Mitra Sayan 
Published: March 2022

AbstractWe present , a tool that uses neural networks for predicting reachable sets from executions of a dynamical system. Unlike existing reachability tools, computes areachability functionthat outputs an accurate over-approximation of the reachable set foranyinitial set in a parameterized family. Such reachability functions are useful for online monitoring, verification, and safe planning. implements empirical risk minimization for learning reachability functions. We discuss the design rationale behind the optimization problem and establish that the computed output is probably approximately correct. Our experimental evaluations over a variety of systems show promise. can learn accurate reachability functions for complex nonlinear systems, including some that are beyond existing methods. From a learned reachability function, arbitrary reachtubes can be computed in milliseconds. is available athttps://github.com/sundw2014/NeuReach.
Kmclib: Automated Inference and Verification of Session Types from OCaml Programs
Authors: Imai Keigo , Lange Julien , Neykova Rumyana 
Published: March 2022

AbstractTheories and tools based on multiparty session types offer correctness guarantees for concurrent programs that communicate using message-passing. These guarantees usually come at the cost of an intrinsically top-down approach, which requires the communication behaviour of the entire program to be specified as a global type.This paper introduces : an OCaml library that supports the development of correct message-passing programs without having to write any types. The library utilises the meta-programming facilities of OCaml to automatically infer the session types of concurrent programs and verify their compatibility (k-MC [15]). Well-typed programs, written with , do not lead to communication errors and cannot get stuck.
Better Counterexamples for Dafny
Authors: Chakarov Aleksandar , Fedchin Aleksandr , Rakamarić Zvonimir , Rungta Neha 
Published: March 2022

AbstractDafny is a verification-aware programming language used at Amazon Web Services to develop critical components of their access management, storage, and cryptography infrastructures. The Dafny toolchain provides a verifier that can prove an implementation of a method satisfies its specification. When the underlying SMT solver cannot establish a proof, it generates a counterexample. These counterexamples are hard to understand and their interpretation is often a bottleneck in the proof debugging process. In this paper, we introduce an open-source tool that transforms counterexamples generated by the SMT solver to a more user-friendly format that maps to the Dafny syntax and is suitable for further processing. This new tool allows the Dafny developers to quickly identify the root cause of a problem with their proof, thereby speeding up the development of Dafny projects.
cvc5: A Versatile and Industrial-Strength SMT Solver
Authors: Barbosa Haniel , Barrett Clark , Brain Martin , Kremer Gereon , Lachnitt Hanna , Mann Makai , Mohamed Abdalrhman , Mohamed Mudathir , Niemetz Aina , Nötzli Andres , Ozdemir Alex , Preiner Mathias , Reynolds Andrew , Sheng Ying , Tinelli Cesare , Zohar Yoni 
Published: March 2022

Abstractcvc5 is the latest SMT solver in the cooperating validity checker series and builds on the successful code base of CVC4. This paper serves as a comprehensive system description of cvc5 ’s architectural design and highlights the major features and components introduced since CVC4 1.8. We evaluate cvc5 ’s performance on all benchmarks in SMT-LIB and provide a comparison against CVC4 and Z3.
Transition Power Abstractions for Deep Counterexample Detection
Authors: Blicha Martin , Fedyukovich Grigory , Hyvärinen Antti E. J. , Sharygina Natasha 
Published: March 2022

AbstractWhile model checking safety of infinite-state systems by inferring state invariants has steadily improved recently, most verification tools still rely on a technique based on bounded model checking to detect safety violations. In particular, the current techniques typically analyze executions by unfolding transitions one step at a time, and the slow growth of execution length prevents detection of deep counterexamples before the tool reaches its limits on computations. We propose a novel model-checking algorithm that is capable of both proving unbounded safety and finding long counterexamples. The idea is to use Craig interpolation to guide the creation of symbolic abstractions ofexponentially longer sequences of transitions. Our experimental analysis shows that on unsafe benchmarks with deep counterexamples our implementation can detect faulty executions that are at least an order of magnitude longer than those detectable by the state-of-the-art tools.
ZDD Boolean Synthesis
Authors: Lin Yi , Tabajara Lucas M. , Vardi Moshe Y. 
Published: March 2022

AbstractMotivated by applications in boolean-circuit design, boolean synthesis is the process of synthesizing a boolean function with multiple outputs, given a relation between its inputs and outputs. Previous work has attempted to solve boolean functional synthesis by converting a specification formula into a Binary Decision Diagram (BDD) and quantifying existentially the output variables. We make use of the fact that the specification is usually given in the form of a Conjunctive Normal Form (CNF) formula, and we can perform resolution on a symbolic representation of a CNF formula in the form of a Zero-suppressed Binary Decision Diagram (ZDD). We adapt the realizability test to the context of CNF and ZDD, and show that theCrossoperation defined in earlier work can be used for witness construction. Experiments show that our approach is complementary to BDD-based Boolean synthesis.
Formal Verification of the Ethereum 2.0 Beacon Chain
Authors: Cassez Franck , Fuller Joanne , Asgaonkar Aditya 
Published: March 2022

AbstractWe report our experience in the formal verification of the reference implementation of the Beacon Chain. The Beacon Chain is the backbone component of the new Proof-of-Stake Ethereum 2.0 network: it is in charge of tracking information about the validators, their stakes, their attestations (votes) and if some validators are found to be dishonest, to slash them (they lose some of their stakes). The Beacon Chain is mission-critical and any bug in it could compromise the whole network. The Beacon Chain reference implementation developed by the Ethereum Foundation is written in Python, and provides a detailed operational description of the state machine each Beacon Chain’s network participant (node) must implement. We have formally specified and verified the absence of runtime errors in (a large and critical part of) the Beacon Chain reference implementation using the verification-friendly language Dafny. During the course of this work, we have uncovered several issues, proposed verified fixes. We have also synthesised functional correctness specifications that enable us to provide guarantees beyond runtime errors. Our software artefact with the code and proofs in Dafny is available at https://github.com/ConsenSys/eth2.0-dafny.
Maximizing Branch Coverage with Constrained Horn Clauses
Authors: Zlatkin Ilia , Fedyukovich Grigory 
Published: March 2022

AbstractState-of-the-art solvers for constrained Horn clauses (CHC) are successfully used to generate reachability facts from symbolic encodings of programs. In this paper, we present a new application to test-case generation: if a block of code is provably unreachable, no test case can be generated allowing to explore other blocks of code. Our new approach uses CHC to incrementally construct different program unrollings and extract test cases from models of satisfiable formulas. At the same time, a CHC solver keeps track of CHCs that represent unreachable blocks of code which makes the unrolling process more efficient. In practice, this lets our approach to terminate early while guaranteeing maximal coverage. Our implementation called Horntinuum exhibits promising performance: it generates high coverage in the majority of cases and spends less time on average than state-of-the-art.
Alpinist: An Annotation-Aware GPU Program Optimizer
Authors: Şakar Ömer , Safari Mohsen , Huisman Marieke , Wijs Anton 
Published: March 2022

AbstractGPU programs are widely used in industry. To obtain the best performance, a typical development process involves the manual or semi-automatic application of optimizations prior to compiling the code. To avoid the introduction of errors, we can augment GPU programs with (pre- and postcondition-style) annotations to capture functional properties. However, keeping these annotations correct when optimizing GPU programs is labor-intensive and error-prone.This paper introduces Alpinist, an annotation-aware GPU program optimizer. It applies frequently-used GPU optimizations, but besides transforming code, it also transforms the annotations. We evaluate Alpinist, in combination with the VerCors program verifier, to automatically optimize a collection of verified programs and reverify them.
Under-Approximating Expected Total Rewards in POMDPs
Authors: Bork Alexander , Katoen Joost-Pieter , Quatmann Tim 
Published: March 2022

AbstractWe consider the problem: is the optimal expected total reward to reach a goal state in a partially observable Markov decision process (POMDP) below a given threshold? We tackle this—generally undecidable—problem by computing under-approximations on these total expected rewards. This is done by abstracting finite unfoldings of the infinite belief MDP of the POMDP. The key issue is to find a suitable under-approximation of the value function. We provide two techniques: a simple (cut-off) technique that uses a good policy on the POMDP, and a more advanced technique (belief clipping) that uses minimal shifts of probabilities between beliefs. We use mixed-integer linear programming (MILP) to find such minimal probability shifts and experimentally show that our techniques scale quite well while providing tight lower bounds on the expected total reward.
AProVE: Non-Termination Witnesses for C Programs
Authors: Hensel Jera , Mensendiek Constantin , Giesl Jürgen 
Published: March 2022

AbstractTo (dis)prove termination of programs, uses symbolic execution to transform the program’s code into an integer transition system, which is then analyzed by several backends. The transformation steps in and the tools in the backend only produce sub-proofs in their domains. Hence, we now developed new techniques to automatically combine the essence of these proofs. If non-termination is proved, then they yield an overall witness, which identifies a non-terminating path in the original program.
GDart: An Ensemble of Tools for Dynamic Symbolic Execution on the Java Virtual Machine (Competition Contribution)
Authors: Mues Malte , Howar Falk 
Published: March 2022

AbstractGDart is an ensemble of tools allowing dynamic symbolic execution of JVM programs. The dynamic symbolic execution engine is decomposed into three different components: a symbolic decision engine (DSE), a concolic executor (SPouT), and a SMT solver backend allowing meta-strategy solving of SMT problems (JConstraints). The symbolic decision component is loosely coupled with the executor by a newly introduced communication protocol. At SV-COMP 2022, GDart solved 471 of 586 tasks finding more correct false results (302) than correct true results (169). It scored fourth place.
Correct Probabilistic Model Checking with Floating-Point Arithmetic
Authors: Hartmanns Arnd 
Published: March 2022

AbstractProbabilistic model checking computes probabilities and expected values related to designated behaviours of interest in Markov models. As a formal verification approach, it is applied to critical systems; thus we trust that probabilistic model checkers deliver correct results. To achieve scalability and performance, however, these tools use finite-precision floating-point numbers to represent and calculate probabilities and other values. As a consequence, their results are affected by rounding errors that may accumulate and interact in hard-to-predict ways. In this paper, we show how to implement fast and correct probabilistic model checking by exploiting the ability of current hardware to control the direction of rounding in floating-point calculations. We outline the complications in achieving correct rounding from higher-level programming languages, describe our implementation as part of the Modest Toolset’s model checker, and exemplify the tradeoffs between performance and correctness in an extensive experimental evaluation across different operating systems and CPU architectures.
Symbiotic-Witch: A Klee-Based Violation Witness Checker
Authors: Ayaziová Paulína , Chalupa Marek , Strejček Jan 
Published: March 2022

AbstractSymbiotic-Witch is a new tool for checking violation witnesses in the GraphML-based format used at SV-COMP since 2015. Roughly speaking, Symbiotic-Witch symbolically executes a given program with Klee and simultaneously tracks the set of nodes the witness automaton can be in. Moreover, it reads the return values of nondeterministic functions specified in the witness and uses them to prune the symbolic execution. The violation witness is confirmed if the symbolic execution reaches an error and the current set of witness nodes contains a matching violation node. Symbiotic-Witch currently supports violation witnesses of reachability safety, memory safety, memory cleanup, and overflow properties.
Correlated Equilibria and Fairness in Concurrent Stochastic Games
Authors: Kwiatkowska Marta , Norman Gethin , Parker David , Santos Gabriel 
Published: March 2022

AbstractGame-theoretic techniques and equilibria analysis facilitate the design and verification of competitive systems. While algorithmic complexity of equilibria computation has been extensively studied, practical implementation and application of game-theoretic methods is more recent. Tools such as PRISM-games support automated verification and synthesis of zero-sum and ($$\varepsilon $$
ε
-optimal subgame-perfect) social welfare Nash equilibria properties for concurrent stochastic games. However, these methods become inefficient as the number of agents grows and may also generate equilibria that yield significant variations in the outcomes for individual agents. We extend the functionality of PRISM-games to support correlated equilibria, in which players can coordinate through public signals, and introduce a novel optimality criterion of social fairness, which can be applied to both Nash and correlated equilibria. We show that correlated equilibria are easier to compute, are more equitable, and can also improve joint outcomes. We implement algorithms for both normal form games and the more complex case of multi-player concurrent stochastic games with temporal logic specifications. On a range of case studies, we demonstrate the benefits of our methods.
On-The-Fly Solving for Symbolic Parity Games
Authors: Laveaux Maurice , Wesselink Wieger , Willemse Tim A. C. 
Published: March 2022

AbstractParity games can be used to represent many different kinds of decision problems. In practice, tools that use parity games often rely on a specification in a higher-order logic from which the actual game can be obtained by means of an exploration. For many of these decision problems we are only interested in the solution for a designated vertex in the game. We formalise how to use on-the-fly solving techniques during the exploration process, and show that this can help to decide the winner of such a designated vertex in an incomplete game. Furthermore, we define partial solving techniques for incomplete parity games and show how these can be made resilient to work directly on the incomplete game, rather than on a set of safe vertices. We implement our techniques for symbolic parity games and study their effectiveness in practice, showing that speed-ups of several orders of magnitude are feasible and overhead (if unavoidable) is typically low.
On Nieh-Yan transport
Authors: Valle Manuel , Vázquez-Mozo Miguel Á. 
Published: March 2022

Abstract
We study nondissipative transport induced by the Nieh-Yan anomaly. After computing the torsional terms in the equilibrium partition function using transgression, we find the constitutive relations for the covariant axial-vector, heat, stress, and spin currents. A number of new transport effects are found, driven by background torsion and the spin chemical potential. Torsional constitutive relations in two-dimensional systems are also analyzed.
Selective cleavage of ncRNA and antiviral activity by RNase2/EDN in THP1-induced macrophages
Authors: Lu Lu , Li Jiarui , Wei Ranlei , Guidi Irene , Cozzuto Luca , Ponomarenko Julia , Prats-Ejarque Guillem , Boix Ester 
Published: March 2022

AbstractRNase2 is the member of the RNaseA family most abundant in macrophages. Here, we knocked out RNase2 in THP-1 cells and analysed the response to Respiratory Syncytial Virus (RSV). RSV induced RNase2 expression, which significantly enhanced cell survival. Next, by cP-RNAseq sequencing, which amplifies the cyclic-phosphate endonuclease products, we analysed the ncRNA population. Among the ncRNAs accumulated in WT vs KO cells, we found mostly tRNA-derived fragments (tRFs) and second miRNAs. Differential sequence coverage identified tRFs from only few parental tRNAs, revealing a predominant cleavage at anticodon and d-loops at U/C (B1) and A (B2) sites. Selective tRNA cleavage was confirmed in vitro using the recombinant protein. Likewise, only few miRNAs were significantly more abundant in WT vs RNase2-KO cells. Complementarily, by screening of a tRF & tiRNA array, we identified an enriched population associated to RNase2 expression and RSV exposure. The results confirm the protein antiviral action and provide the first evidence of its cleavage selectivity on ncRNAs.
Graphical abstract
Akutes Kompartmentsyndrom der Extremitäten
Authors: Kalbas Y. , Kumabe Y. , Sellei R. M. , Pape H. C. 
Published: March 2022

ZusammenfassungDas akute Kompartmentsyndrom der Extremitäten ist ein chirurgischer Notfall, dessen schnelle Diagnose und sofortige operative Therapie essenziell für das Outcome sind. Ursächlich ist ein Anstieg des Gewebedruckes innerhalb einer durch Faszien eingeschlossenen Muskelloge und eine daraus resultierende Mikroperfusionsstörung. Diese kann potenziell desaströse Folgen, wie den Verlust der Extremität durch großflächige Nekrosen oder eine vitale Bedrohung durch infektiöse Komplikationen, haben. Obwohl meist traumatisch bedingt, kann auch eine Vielzahl anderer Ursachen zur Entstehung eines Kompartmentsyndroms führen, sodass eine Grundkenntnis dieses Zustandsbildes nicht nur für Unfallchirurgen von großer Wichtigkeit ist. Dies gilt vor allem, weil eine zeitige Therapie eine schnelle Diagnose- und Indikationsstellung erfordert. Im folgenden Artikel wird ein Überblick über die zugrunde liegende Pathophysiologie, die Ursachen, die Symptome sowie die Therapie des akuten Kompartmentsyndroms dargestellt.