Tools and Algorithms for the Construction and Analysis of Systems
28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2–7, 2022, Proceedings, Part I
- Open Access
- 2022
- Open Access
- Buch
- Herausgegeben von
- Dr. Dana Fisman
- Grigore Rosu
- Buchreihe
- Lecture Notes in Computer Science
- Verlag
- Springer International Publishing
Über dieses Buch
Dieses Open-Access-Buch stellt die Tagung der 28. Internationalen Konferenz über Werkzeuge und Algorithmen für die Konstruktion und Analyse von Systemen, TACAS 2022, dar, die vom 2. bis 7. April 2022 im Rahmen der Europäischen Gemeinsamen Konferenzen zur Theorie und Praxis von Software, ETAPS 2022, in München stattfand. Die 46 vollständigen und 4 kurzen Beiträge in diesem Band wurden sorgfältig geprüft und aus 159 Einreichungen ausgewählt. Das Verfahren umfasst auch 16 Toolpapers des angeschlossenen Wettbewerbs SV-Comp und 1 Paper bestehend aus dem Wettbewerbsbericht. TACAS ist ein Forum für Forscher, Entwickler und Anwender, die sich für streng basierte Werkzeuge und Algorithmen zum Aufbau und zur Analyse von Systemen interessieren. Die Konferenz zielt darauf ab, die Kluft zwischen verschiedenen Gemeinschaften mit diesem gemeinsamen Interesse zu überbrücken und sie in ihrem Bestreben zu unterstützen, die Nützlichkeit, Zuverlässigkeit, Flexibilität und Effizienz von Werkzeugen und Algorithmen zum Aufbau computergesteuerter Systeme zu verbessern.
Mit KI übersetzt
Über dieses Buch
This open access book constitutes the proceedings of the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2022, which was held during April 2-7, 2022, in Munich, Germany, as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022.
The 46 full papers and 4 short papers presented in this volume were carefully reviewed and selected from 159 submissions. The proceedings also contain 16 tool papers of the affiliated competition SV-Comp and 1 paper consisting of the competition report.
TACAS is a forum for researchers, developers, and users interested in rigorously based tools and algorithms for the construction and analysis of systems. The conference aims to bridge the gaps between different communities with this common interest and to support them in their quest to improve the utility, reliability, exibility, and efficiency of tools and algorithms for building computer-controlled systems.
Anzeige
Inhaltsverzeichnis
-
Synthesis
-
Frontmatter
-
HOLL: Program Synthesis for Higher Order Logic Locking
- Open Access
PDF-Version jetzt herunterladenDas Kapitel diskutiert die Bedrohung durch Fälschung und Piraterie in der Halbleiterindustrie und führt als Lösung Higher Order Logic Locking (HOLL) ein. HOLL verbirgt eine Beziehung höherer Ordnung anstelle einer Abfolge unabhängiger Schlüsselbits, was es sicherer gegen Angriffe wie den SAT-Angriff macht. Die Autoren schlagen einen neuen Angriff vor, SynthAttack, um die Sicherheit von HOLL zu bewerten und seine Wirksamkeit zu demonstrieren. Das Kapitel behandelt auch die Implementierung und Optimierung von HOLL, wobei der geringe Aufwand und die Widerstandsfähigkeit gegen bestehende Angriffe hervorgehoben werden.KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
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. -
The Complexity of LTL Rational Synthesis
- Open Access
PDF-Version jetzt herunterladenDas Kapitel vertieft sich in die Komplexität der rationalen LTL-Synthese, eines Prozesses, der automatisch reaktive Systeme konstruiert, um deren Spezifikationen auch in rationalen Umgebungen zu erfüllen. Es baut auf früheren Arbeiten auf, um die Obergrenzen für Einstellungen mit drei oder mehr Spielern und gleichzeitigen Spielen zu verschärfen. Die Komplexitätsanalyse ist parametrisch, unter Berücksichtigung des Spieldiagramms, der Ziele der Systemkomponenten und der Ziele der Umweltkomponenten. Die Studie verallgemeinert die rationale Synthese, indem sie kooperative und nicht kooperative Ansätze kombiniert und die Komplexitätsanalyse auf diese umfassendere Definition ausweitet. Insbesondere werden Algorithmen eingeführt, die die rationale Synthese auf das Nichtleerheitsproblem von Baumautomaten reduzieren und ein detailliertes und differenziertes Verständnis der damit verbundenen rechnerischen Herausforderungen liefern.KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
AbstractIn rational synthesis, we automatically construct a reactive system that satisfies its specification in all rational environments, namely environments that have objectives and act to fulfill them. We complete the study of the complexity of LTL rational synthesis. Our contribution is threefold. First, we tighten the known upper bounds for settings that were left open in earlier work. Second, our complexity analysis is parametric, and we describe tight upper and lower bounds in each of the problem parameters: the game graph, the objectives of the system components, and the objectives of the environment components. Third, we generalize the definition of rational synthesis, combining the cooperative and non-cooperative approaches studied in earlier work, and extend our complexity analysis to the general definition. -
Synthesis of Compact Strategies for Coordination Programs
- Open Access
PDF-Version jetzt herunterladenDas Kapitel "Synthese kompakter Strategien für Koordinierungsprogramme" von Kedar S. Namjoshi und Nisarg Patel befasst sich mit dem entscheidenden Thema der Synthese von Koordinierungsstrategien, die garantiert keine unnötigen Aktionen in Multiagenten-Umgebungen wie IoT und Robotik auslösen. Aktuelle Methoden können Strategien hervorbringen, die nutzlose Aktionen auslösen, was die Koordination zu einem attraktiven Ziel für die automatisierte Programmsynthese macht. Die Autoren formalisieren den Begriff der "Kompaktheit" und schlagen eine Lösung vor, die eine vorgegebene zeitliche Logik mithilfe automatiatentheoretischer Konstruktionen transformiert, um einen Begriff der Minimalität einzubeziehen. Das zentrale Ergebnis ist, dass die Gewinnstrategien für die transformierte Spezifikation genau die kompakten Strategien für das Original sind. Dies ermöglicht die Anwendung bekannter Synthesemethoden, um kompakte Strategien zu entwickeln. Das Kapitel berichtet über Prototypimplementierungen und Experimente, die die Machbarkeit und Effektivität der vorgeschlagenen Methoden belegen. Außerdem wird die Beziehung zur quantitativen Synthese diskutiert und Approximationsmethoden vorgestellt, um die Komplexität der Synthese kompakter Strategien zu bewältigen. Die Arbeit lenkt die Aufmerksamkeit auf die Notwendigkeit der Kompaktheit bei der Programmsynthese und liefert eine präzise Formulierung und praktische Algorithmen, um diese zu erreichen.KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
AbstractIn multi-agent settings, such as IoT and robotics, it is necessary to coordinate the actions of independent agents in order to achieve a joint behavior. While it is often easy to specify the desired joint behavior, programming the necessary coordination can be difficult. In this work, we develop theory and methods to synthesize coordination strategies that are guaranteed not to initiate unnecessary actions. We refer to such strategies as being “compact.” We formalize the intuitive notion of compactness; show that existing methods do not guarantee compactness; and propose a solution. The solution transforms a given temporal logic specification, using automata-theoretic constructions, to incorporate a notion of minimality. The central result is that the winning strategies for the transformed specification are precisely the compact strategies for the original. One can therefore apply known synthesis methods to produce compact strategies. We report on prototype implementations that synthesize compact strategies for temporal logic specifications and for specifications of multi-robot coordination. -
ZDD Boolean Synthesis
- Open Access
PDF-Version jetzt herunterladenDas Kapitel behandelt die Anwendung von Zero-Suppressed Binary Decision Diagrams (ZDDs) in der booleschen Synthese, einem Prozess, der für elektronische Schaltungen und Rechner von entscheidender Bedeutung ist. Es vergleicht ZDDs mit Binären Entscheidungsdiagrammen (BDDs) und zeigt, dass ZDDs kompaktere Darstellungen und schnellere Kompilierungszeiten bieten können. Die Autoren stellen eine umfassende Untersuchung vor, in der Größe und Leistung von ZDDs und BDDs verglichen werden, wobei der Schwerpunkt auf Realisierbarkeit, Zeugenbau und End-to-End-Synthese liegt. Experimentelle Ergebnisse zeigen, dass keiner der Ansätze über alle Benchmarks hinweg dominiert, ZDDs jedoch in bestimmten skalierbaren Formelfamilien herausragen. Dies macht das Kapitel zu einer wertvollen Ressource für Forscher und Praktiker in der booleschen Logik und im Schaltungsdesign und bietet Einblicke in das Potenzial von ZDDs als ergänzendes Werkzeug in der booleschen Synthese.KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
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 the Cross operation defined in earlier work can be used for witness construction. Experiments show that our approach is complementary to BDD-based Boolean synthesis.
-
-
Verification
-
Frontmatter
-
Comparative Verification of the Digital Library of Mathematical Functions and Computer Algebra Systems
- Open Access
PDF-Version jetzt herunterladenDas Kapitel konzentriert sich auf den Vergleich und die Verifikation der Digitalen Bibliothek Mathematischer Funktionen (DLMF) und zweier Allzweck-Computeralgebra-Systeme (CAS), Maple und Mathematica. Die Autoren stellen einen neuartigen Ansatz vor, um mathematische Ausdrücke aus dem DLMF mithilfe ihres zuvor entwickelten Tools LACAST in diesen CAS zu übersetzen. Die Studie beleuchtet die Herausforderungen und Lösungen bei der Übersetzung mathematischer Ausdrücke, insbesondere die semantische Mehrdeutigkeit mathematischer Notationen. Die Autoren befassen sich mit Fragen im Zusammenhang mit der Übersetzung von Summen, Produkten, Integralen, Grenzen und Differenzierungen und verbessern so die Zuverlässigkeit und Reichweite der Übersetzungen. Der Aufsatz bietet auch eine eingehende Bewertung des DLMF anhand sowohl symbolischer als auch numerischer Auswertungen in Maple und Mathematica. Die Ergebnisse zeigen die Machbarkeit und die Grenzen des Übersetzungsansatzes auf und zeigen das Potenzial zur Verbesserung und Verifizierung digitaler mathematischer Bibliotheken und CAS auf. Das Kapitel schließt mit der Bereitstellung eines offenen Zugangs zu allen Übersetzungen und dem Quellcode von LACAST, was es zu einer wertvollen Ressource für Forscher und Praktiker auf diesem Gebiet macht.KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
AbstractDigital mathematical libraries assemble the knowledge of years of mathematical research. Numerous disciplines (e.g., physics, engineering, pure and applied mathematics) rely heavily on compendia gathered findings. Likewise, modern research applications rely more and more on computational solutions, which are often calculated and verified by computer algebra systems. Hence, the correctness, accuracy, and reliability of both digital mathematical libraries and computer algebra systems is a crucial attribute for modern research. In this paper, we present a novel approach to verify a digital mathematical library and two computer algebra systems with one another by converting mathematical expressions from one system to the other. We use our previously developed conversion tool (referred to as
) to translate formulae from the NIST Digital Library of Mathematical Functions to the computer algebra systems MapleandMathematica. The contributions of our presented work are as follows: (1) we present the most comprehensive verification of computer algebra systems and digital mathematical libraries with one another; (2) we significantly enhance the performance of the underlying translator in terms of coverage and accuracy; and (3) we provide open access to translations forMapleandMathematicaof the formulae in the NIST Digital Library of Mathematical Functions. -
Verifying Fortran Programs with CIVL
- Open Access
PDF-Version jetzt herunterladenDas Kapitel behandelt die Erweiterung des CIVL-Verifikationsrahmens auf Fortran-Programme, eine Sprache, die in der Computerwissenschaft und im Hochleistungsrechner weit verbreitet ist. Die Erweiterung ermöglicht es CIVL, Fortran-Quelldateien direkt zu konsumieren, unterstützt Funktionen wie Array-Slicing und Umformung und findet Fortran-spezifische Programmverletzungen. Die Autoren demonstrieren die Effektivität des Tools anhand einer Verifikationsbenchmark-Suite und realer Anwendungskerne und zeigen seine Fähigkeit, funktionale Korrektheiten zu überprüfen und Fehler zu erkennen. Das Kapitel beleuchtet auch die Herausforderungen bei der Erhaltung von Fehlern während der Übersetzung und die Bedeutung statischer Analysen im Verifikationsprozess.KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
AbstractFortran is widely used in computational science, engineering, and high performance computing. This paper presents an extension to the CIVL verification framework to check correctness properties of Fortran programs. Unlike previous work that translates Fortran to C, LLVM IR, or other intermediate formats before verification, our work allows CIVL to directly consume Fortran source files. We extended the parsing, translation, and analysis phases to support Fortran-specific features such as array slicing and reshaping, and to find program violations that are specific to Fortran, such as argument aliasing rule violations, invalid use of variable and function attributes, or defects due to Fortran’s unspecified expression evaluation order. We demonstrate the usefulness of our tool on a verification benchmark suite and kernels extracted from a real world application. -
NORMA: a tool for the analysis of Relay-based Railway Interlocking Systems
- Open Access
PDF-Version jetzt herunterladenDas Kapitel stellt Norma vor, ein Werkzeug zur Analyse von Relais-basierten Railway Interlocking Systems (RRIS). Norma wurde mit Mitteln des italienischen Eisenbahnnetzes entwickelt und unterstützt das Reverse Engineering und die Migration alter RRIS-Systeme auf moderne computergestützte Systeme. Es verfügt über eine grafische Modellierungsschnittstelle mit über 200 konfigurierbaren Komponenten und nutzt formale Verifikationstechniken, um syntaktische und semantische Überprüfungen, Simulationen und die Extraktion von Eigenschaften bereitzustellen. Die interne Darstellung von Norma wird in hochgradig optimierte Timed nuXmv-Modelle übersetzt, die eine effiziente Verifizierung und Analyse ermöglichen. Das Tool wurde experimentell anhand von RRIS-Schaltplänen aus der realen Welt ausgewertet, was seine Effektivität bei der Unterstützung von Modellierern und der Verkürzung von Verifikationszeiten gezeigt hat. Normas einzigartiger Ansatz zur komponentenbasierten Modellierung und die Integration leistungsstarker Argumentationsfähigkeiten machen es zu einem herausragenden Werkzeug in diesem Bereich.KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
AbstractWe present Norma, a tool for the modeling and analysis of Relay-based Railways Interlocking Systems (RRIS). Norma is the result of a research project funded by the Italian Railway Network, to support the reverse engineering and migration to computer-based technology of legacy RRIS. The frontend fully supports the graphical modeling of Italian RRIS, with a palette of over two hundred basic components, stubs to abstract RRIS subcircuits, and requirements in terms of formal properties. The internal component based representation is translated into highly optimized Timed nuXmv models, and supports various syntactic and semantic checks based on formal verification, simulation and test case generation. Norma is experimentally evaluated, demonstrating the practical support for the modelers, and the effectiveness of the underlying optimizations. -
Efficient Neural Network Analysis with Sum-of-Infeasibilities
- Open Access
PDF-Version jetzt herunterladenDas Kapitel stellt eine neue Methode zur Analyse von Abfragen zur Überprüfung neuronaler Netzwerke mittels der Sum-of-Infeasibilities (SoI) -Technik vor. Inspiriert von Methoden der konvexen Optimierung misst die SoI-Funktion den Fehler in den Aktivierungsfunktionen und leitet die Suche nach befriedigenden Aufgaben in einer konvexen Entspannung des Netzwerks. Die Autoren schlagen DeepSoI vor, ein stochastisches Verfahren, das die SoI durch Markov-Ketten-Monte-Carlo-Probenahme minimiert und ihre Integration in ein vollständiges Verifikationsverfahren demonstriert. Das Kapitel hebt die Vorteile des SoI-basierten Ansatzes durch umfangreiche experimentelle Evaluierung hervor und zeigt signifikante Leistungsverbesserungen gegenüber bestehenden Methoden. Darüber hinaus präsentieren die Autoren einen interessanten Anwendungsfall zur Verbesserung der Störungsgrenzen, die durch feindliche Angriffsalgorithmen gefunden werden.KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
AbstractInspired by sum-of-infeasibilities methods in convex optimization, we propose a novel procedure for analyzing verification queries on neural networks with piecewise-linear activation functions. Given a convex relaxation which over-approximates the non-convex activation functions, we encode the violations of activation functions as a cost function and optimize it with respect to the convex relaxation. The cost function, referred to as the Sum-of-Infeasibilities (SoI), is designed so that its minimum is zero and achieved only if all the activation functions are satisfied. We propose a stochastic procedure, DeepSoI, to efficiently minimize the SoI. An extension to a canonical case-analysis-based complete search procedure can be achieved by replacing the convex procedure executed at each search state with DeepSoI. Extending the complete search with DeepSoI achieves multiple simultaneous goals: 1) it guides the search towards a counter-example; 2) it enables more informed branching decisions; and 3) it creates additional opportunities for bound derivation. An extensive evaluation across different benchmarks and solvers demonstrates the benefit of the proposed techniques. In particular, we demonstrate that SoI significantly improves the performance of an existing complete search procedure. Moreover, the SoI-based implementation outperforms other state-of-the-art complete verifiers. We also show that our technique can efficiently improve upon the perturbation bound derived by a recent adversarial attack algorithm.
-
-
Blockchain
-
Frontmatter
-
Formal Verification of the Ethereum 2.0 Beacon Chain
- Open Access
PDF-Version jetzt herunterladenDas Kapitel "Formal Verification of the Ethereum 2.0 Beacon Chain" von Franck Cassez, Joanne Fuller und Aditya Asgaonkar geht der formalen Verifizierung der Ethereum 2.0 Beacon Chain nach, einem zentralen Bestandteil des neuen Proof-of-Stake-Ethereum-Netzwerks. Die Autoren erläutern ihre Methodik anhand der verifizierungsfreundlichen Sprache Dafny, um die Abwesenheit von Laufzeitfehlern in der Referenzimplementierung zu überprüfen. Sie deckten mehrere Probleme auf, schlugen überprüfte Lösungen vor und erstellten Spezifikationen für die funktionale Korrektheit. Das Kapitel unterstreicht die Bedeutung einer formalen Verifizierung, um die Sicherheit und Zuverlässigkeit der Beacon Chain zu gewährleisten, die eine enorme Menge an Vermögenswerten verwaltet und für das Ökosystem Ethereum 2.0 von entscheidender Bedeutung ist. Die Autoren diskutieren auch die Herausforderungen und Lektionen, die während des Verifikationsprozesses gelernt wurden, und geben wertvolle Einblicke in die praktische Anwendung formaler Methoden in der Blockchain-Technologie.KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
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. -
Fast and Reliable Formal Verification of Smart Contracts with the Move Prover
- Open Access
PDF-Version jetzt herunterladenDer Move Prover (MVP) ist ein formales Überprüfungswerkzeug für intelligente Verträge, die in der Programmiersprache Move geschrieben sind und in der Diem Blockchain verwendet werden. Das Kapitel behandelt die Herausforderungen und Lösungen, die MVP schnell und zuverlässig machen, einschließlich eines alias-freien Speichermodells, feinkörniger invarianter Prüfung und Monomorphisierung. Diese Verbesserungen haben die Verifikationszeiten und Timeouts deutlich reduziert, wodurch MVP für den Routineeinsatz durch Entwickler praktisch ist. Das Kapitel untersucht auch das Design von MVP und seiner Spezifikationssprache, die aussagekräftige Spezifikationen und Invarianten unterstützt. Der Move Prover wurde erfolgreich zur Verifizierung großer Teile des Diem-Rahmenwerks eingesetzt und ist in den kontinuierlichen Integrationsprozess integriert, wodurch die Zuverlässigkeit intelligenter Verträge gewährleistet ist.KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
AbstractThe Move Prover (MVP) is a formal verifier for smart contracts written in the Move programming language. MVP has an expressive specification language, and is fast and reliable enough that it can be run routinely by developers and in integration testing. Besides the simplicity of smart contracts and the Move language, three implementation approaches are responsible for the practicality of MVP: (1) an alias-free memory model, (2) fine-grained invariant checking, and (3) monomorphization. The entirety of the Move code for the Diem blockchain has been extensively specified and can be completely verified by MVP in a few minutes. Changes in the Diem framework must be successfully verified before being integrated into the open source repository on GitHub. -
A Max-SMT Superoptimizer for EVM handling Memory and Storage
- Open Access
PDF-Version jetzt herunterladenDas Kapitel stellt GASOLv2 vor, einen Superoptimierer für intelligente Ethereum-Verträge, der sowohl den Gasverbrauch als auch die Byte-Größe optimiert. Es nutzt einen Max-SMT-Ansatz zur Handhabung von Speicher- und Speicheroperationen und adressiert Herausforderungen, die bisher ungelöst waren. Das Tool wurde entwickelt, um mit dem Solidity Compiler Solc zu arbeiten und hat deutliche Verbesserungen bei der Optimierung gezeigt. Das Kapitel behandelt die Architektur und die Komponenten von GASOLv2, einschließlich der Synthese von Stack- und Speicherspezifikationen, Vereinfachungsregeln und der Verwendung eines Max-SMT-Solvers zur Optimierung. Die Autoren präsentieren experimentelle Ergebnisse, die die Effektivität von GASOLv2 bei der Erzielung erheblicher Zuwächse beim Gasverbrauch und der Optimierung der Byte-Größe belegen. Das Kapitel beleuchtet auch die praktischen Auswirkungen des Umgangs mit Speicheroperationen bei der Superoptimierung und das Potenzial für weitere Verbesserungen in diesem Bereich.KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
AbstractSuperoptimization is a compilation technique that searches for the optimal sequence of instructions semantically equivalent to a given (loop-free) initial sequence. With the advent of SMT solvers, it has been successfully applied to LLVM code (to reduce the number of instructions) and to Ethereum EVM bytecode (to reduce its gas consumption). Both applications, when proven practical, have left out memory operations and thus missed important optimization opportunities. A main challenge to superoptimization today is handling memory operations while remaining scalable. We present \(\textsf {GASOL}^{v2}\), a gas and bytes-size superoptimization tool for Ethereum smart contracts, that leverages a previous Max-SMT approach for only stack optimization to optimize also wrt. memory and storage. \(\textsf {GASOL}^{v2}\) can be used to optimize the size in bytes, aligned with the optimization criterion used by the Solidity compiler solc, and it can also be used to optimize gas consumption. Our experiments on 12,378 blocks from 30 randomly selected real contracts achieve gains of 16.42% in gas wrt. the previous version of the optimizer without memory handling, and gains of 3.28% in bytes-size over code already optimized by solc.
-
-
Grammatical Inference
-
Frontmatter
-
A New Approach for Active Automata Learning Based on Apartness
- Open Access
PDF-Version jetzt herunterladenDas Kapitel stellt eine neue Methode für aktives automatisches Lernen vor, die L # genannt wird und sich auf die Etablierung von Zweisamkeit und nicht auf die Äquivalenz von Beobachtungen konzentriert. Dieser Ansatz vereinfacht den Lernprozess, indem er direkt auf einem Beobachtungsbaum operiert, und vermeidet die Notwendigkeit zusätzlicher Datenstrukturen wie Beobachtungstabellen. Der L # -Algorithmus hat die gleichen asymptotischen Abfrage- und Symbolkomplexitäten wie die besten bestehenden Lernalgorithmen, integriert aber adaptive Unterscheidungssequenzen, um die Leistung zu steigern. Experimente mit einer Prototyp-Implementierung legen nahe, dass L # mit hoch optimierten Algorithmen konkurrenzfähig ist. Das Kapitel behandelt auch verwandte Arbeiten, einschließlich anderer Ansätze für aktives automatisches Lernen und die Integration von Konformitätstests zur Steigerung der Lerneffizienz.KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
AbstractWe present \(L^{\#}\), a new and simple approach to active automata learning. Instead of focusing on equivalence of observations, like the \(L^{*}\) algorithm and its descendants, \(L^{\#}\) takes a different perspective: it tries to establish apartness, a constructive form of inequality. \(L^{\#}\) does not require auxiliary notions such as observation tables or discrimination trees, but operates directly on tree-shaped automata. \(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^{\#}\) in practice. Experiments with a prototype implementation, written in Rust, suggest that \(L^{\#}\) is competitive with existing algorithms. -
Learning Realtime One-Counter Automata
- Open Access
PDF-Version jetzt herunterladenIn diesem Kapitel wird ein neuartiger Algorithmus zum Erlernen von Ein-Zählautomaten in Echtzeit vorgestellt, die aussagekräftigere Modelle sind als endliche Zustandsautomaten. Der Algorithmus erweitert Angluins L х -Algorithmus durch die Einbeziehung von Gegenwert- und Teiläquivalenzabfragen, wodurch er in die Lage versetzt wird, komplexere Systeme zu handhaben. Die Autoren beweisen, dass ihr Algorithmus exponentiell in Zeit und Raum abläuft, und sie bewerten ihn durch Experimente mit zufälligen Benchmarks und einem Anwendungsfall, bei dem JSON-Stream validiert wird. In diesem Kapitel werden auch die Herausforderungen und zukünftigen Arbeiten bei der Verfeinerung des Algorithmus und seiner Anwendungen diskutiert.KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
AbstractWe present a new learning algorithm for realtime one-counter automata. Our algorithm uses membership and equivalence queries as in Angluin’s \({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
- Open Access
PDF-Version jetzt herunterladenDas Kapitel stellt einen neuartigen Algorithmus zum Erlernen von Formeln in Fragmenten der Linearen Temporalen Logik (LTL) ohne U-Operator vor, der sich mit der Skalierbarkeit und den Rechenressourcenproblemen bestehender Methoden befasst. Der Algorithmus ist jederzeit einsetzbar, d.h. er kann Trennformeln herstellen, auch wenn er mal ausfällt, und er verwendet eine Kombination gerichteter Formeln und boolescher Kombinationen, um diese Formeln effizient zu konstruieren. Die Autoren demonstrieren die Effektivität und Skalierbarkeit des Algorithmus durch empirische Auswertungen und zeigen, dass er bestehende Werkzeuge sowohl in der Geschwindigkeit als auch in der Größe der Formeln, die er lernen kann, übertrifft. In diesem Kapitel werden auch die theoretischen Garantien des Algorithmus und sein Potenzial für zukünftige Erweiterungen zur vollständigen LTL diskutiert.KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
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}\)-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. -
Learning Model Checking and the Kernel Trick for Signal Temporal Logic on Stochastic Processes
- Open Access
PDF-Version jetzt herunterladenDas Kapitel behandelt die Anwendung des Kernel-Tricks auf Formeln der Signalzeitlogik (STL), die ein effizientes Lernen und die Vorhersage der Formelzufriedenheit bei stochastischen Prozessen ermöglichen. Die Autoren stellen eine Kernfunktion für STL vor, die die Umgehung der manuellen Feature-Extraktion ermöglicht, was die hohe Präzision und Recheneffizienz ihres Ansatzes demonstriert. Das Kapitel bietet auch eine theoretische Analyse mit einer PAC-Grenze, die eine nahezu optimale Leistung ihres Prädiktors gewährleistet. Die Autoren bewerten ihre Methode durch Experimente und zeigen ihre praktische Anwendbarkeit auf verschiedene stochastische Prozesse und Formeln aus der realen Welt.KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
AbstractWe introduce a similarity function on formulae of signal temporal logic (STL). It comes in the form of a kernel function, well known in machine learning as a conceptually and computationally efficient tool. The corresponding kernel trick allows us to circumvent the complicated process of feature extraction, i.e. the (typically manual) effort to identify the decisive properties of formulae so that learning can be applied. We demonstrate this consequence and its advantages on the task of predicting (quantitative) satisfaction of STL formulae on stochastic processes: Using our kernel and the kernel trick, we learn (i) computationally efficiently (ii) a practically precise predictor of satisfaction, (iii) avoiding the difficult task of finding a way to explicitly turn formulae into vectors of numbers in a sensible way. We back the high precision we have achieved in the experiments by a theoretically sound PAC guarantee, ensuring our procedure efficiently delivers a close-to-optimal predictor.
-
- Titel
- Tools and Algorithms for the Construction and Analysis of Systems
- Herausgegeben von
-
Dr. Dana Fisman
Grigore Rosu
- Copyright-Jahr
- 2022
- Electronic ISBN
- 978-3-030-99524-9
- Print ISBN
- 978-3-030-99523-2
- DOI
- https://doi.org/10.1007/978-3-030-99524-9
Informationen zur Barrierefreiheit für dieses Buch folgen in Kürze. Wir arbeiten daran, sie so schnell wie möglich verfügbar zu machen. Vielen Dank für Ihre Geduld.
