The proceedings contain 39 papers. The special focus in this conference is on logic for programming, Artificial Intelligence and Reasoning. The topics include: When are two gossips the same?;function summarization mod...
The proceedings contain 39 papers. The special focus in this conference is on logic for programming, Artificial Intelligence and Reasoning. The topics include: When are two gossips the same?;function summarization modulo theories;matching in the description logic fl0 with respect to general tboxes;lyndon interpolation holds for the prenex ⊃ prenex fragment of gödel logic;decidable inequalities over infinite trees;evaluation of domain agnostic approaches for enumeration of minimal unsatisfiable subsets;why these automata types?;a verified efficient implementation of the lll basis reduction algorithm;efficient sat-based encodings of conditional cardinality constraints;reasoning about prescription and description using prioritized default rules;two-variable first-order logic with counting in forests;quasipolynomial set-based symbolic algorithms for parity games;the involutions-as-principal types/ application-as-unification analogy;left-handed completeness for kleene algebra, via cyclic proofs∗;experiments in verification of linear model predictive control: Automatic generation and formal verification of an interior point method algorithm∗;graph path orderings;the weak completion semantics and equality;ltl with arithmetic and its applications in reasoning about hierarchical systems;arrays made simpler: An efficient, scalable and thorough preprocessing;loop analysis by quantification over iterations;formal verification of the yubikey and yubihsm apis in maude-npa∗;lookahead-based smt solving;a complete cyclic proof system for inductive entailments in first order logic;towards smarter mace-style model finders;improving sat-based bounded model checking for existential ctl through path reuse;is satisfiability of quantified bit-vector formulas stable under bit-width changes?∗;alternating reachability games with behavioral and revenue objectives;polymorphic success types for erlang.
The proceedings contain 18 papers. The special focus in this conference is on Applications of Declarative programming and Knowledge Management. The topics include: Facets of the PIE Environment for Proving, Interpolat...
ISBN:
(纸本)9783030467135
The proceedings contain 18 papers. The special focus in this conference is on Applications of Declarative programming and Knowledge Management. The topics include: Facets of the PIE Environment for Proving, Interpolating and Eliminating on the Basis of First-Order logic;KBSET – Knowledge-Based Support for Scholarly Editing and Text Processing with Declarative Markup and a Core Written in SWI-Prolog;structured Traversal of Search Trees in Constraint-logic Object-Oriented programming;performance Analysis of Zippers;adding Data to Curry;free Theorems Simply, via Dinaturality;Improving the Performance of the Paisley Pattern-Matching EDSL by Staged Combinatorial Compilation;ICurry;a Process Calculus for Formally Verifying Blockchain Consensus Protocols;modular Modeling and Optimized Scheduling of Building Energy Systems Based on Mixed Integer programming;finding Maximal Non-redundant Association Rules in Tennis Data;from Textual Information Sources to Linked Data in the Agatha Project;allen’s Interval Algebra Makes the Difference;exploring Properties of Icosoku by Constraint Satisfaction Approach;the Regularization of Small Sub-Constraint Satisfaction Problems;declarative programming for Microcontrollers - Datalog on Arduino.
The proceedings contain 11 papers. The topics discussed include: automatically generated supernodes for AST interpreters improve virtual-machine performance;a monadic framework for name resolution in multi-phased type...
ISBN:
(纸本)9798400704062
The proceedings contain 11 papers. The topics discussed include: automatically generated supernodes for AST interpreters improve virtual-machine performance;a monadic framework for name resolution in multi-phased type checkers;C2TACO: lifting tensor code to TACO;partial evaluation of automatic differentiation for differential-algebraic equations solvers;crossover: towards compiler-enabled COBOL-C interoperability;generating conforming programs with Xsmith;multi-stage vertex-centric programming for agent-based simulations;unleashing the power of implicit feedback in software product lines: benefits ahead;virtual domain specific languages via embedded projectional editing;and generating constraint programs for variability model reasoning: a DSL and solver-agnostic approach.
The proceedings contain 15 papers. The topics discussed include: formal design of cyber-physical systems with learning-enabled components;on challenges and opportunities in the translation of deep neural networks into...
The proceedings contain 15 papers. The topics discussed include: formal design of cyber-physical systems with learning-enabled components;on challenges and opportunities in the translation of deep neural networks into finite automata;towards machine learning enhanced LTL monitoring;towards large language model architectures for knowledge acquisition and strategy synthesis;ODD-based health monitoring and predictive maintenance of degrading vehicle functionality;a first-order interval temporal logic for adjacent variables temporal data;heuristic minimization modulo theory of modal decision trees class-formulas;revisiting formal verification in VeriSolid: an analysis and enhancements;towards compliance of smart contracts with the European union data act;and tree kernels to support formal methods-based testing of evolving specifications.
Robots and IoT devices must process real-time signals using embedded systems with limited power and clock speeds rather than large CPUs or GPUs. FPGAs offer highly parallel computation, but are difficult to program, b...
详细信息
ISBN:
(纸本)9798350381993;9798350382006
Robots and IoT devices must process real-time signals using embedded systems with limited power and clock speeds rather than large CPUs or GPUs. FPGAs offer highly parallel computation, but are difficult to program, both algorithmically and at hardware implementation level. Programmers of digital signal processing (DSP), machine vision, and neural networks typically work in high level, serial languages such as Python, so would benefit from a tool to automatically convert this code to run on FPGA. We present a design for a compiler from a serial Python subset to parallel dataflow FPGA, in which the physical connectivity and dataflow of the digital logic mirrors the logical dataflow of the programs. The subset removes some imperative features from Python and focuses on Python's functional programming elements, which can be more easily compiled into physical digital logic implementations of dataflows. Some imperative features are retained but interpreted under alternative functional semantics, making them easier to parallelize. These dataflows can then be pipelined for efficient continuous real-time data processing. An open-source partial implementation is provided together with a compilable simple neuron program.
The proceedings contain 19 papers. The topics discussed include: on computational problems for infinite argumentation frameworks: the complexity of finding acceptable extensions;linear algebraic partial evaluation of ...
The proceedings contain 19 papers. The topics discussed include: on computational problems for infinite argumentation frameworks: the complexity of finding acceptable extensions;linear algebraic partial evaluation of logic programs;probabilistic logicprogramming under the l-stable semantics;walking the tightrope between expressiveness and uncomputability: AGM contraction beyond the finitary realm;reasoning about simultaneous change in trust and belief;an extension-based argument-ranking semantics: social rankings in abstract argumentation;defining an adaptable framework for behavior support agents in default logic;a first peek into preferential logics with team semantics;extraction of conditional belief bases and the system Z ranking model from multilayer perceptrons for binary classification;and on the correspondence of non-flat assumption-based argumentation andlogicprogramming with negation as failure in the head.
Pragmatic Action Charts are a minimalist Statecharts variant that can be implemented relatively easily as internal DSL in most mainstream languages. In this paper, they are implemented as internal DSL leveraging the o...
详细信息
ISBN:
(数字)9798350378023
ISBN:
(纸本)9798350378030;9798350378023
Pragmatic Action Charts are a minimalist Statecharts variant that can be implemented relatively easily as internal DSL in most mainstream languages. In this paper, they are implemented as internal DSL leveraging the object-oriented paradigm of the host language avoiding the introduction of yet another programming language. Internal DSLS can also benefit from appropriate instantaneous visualizations, which is usually attributed to specialized, graphical DSLS. Pragmatic Action Trees use the same minimalist approach to integrate behavior trees into an arbitrary host language. To achieve this, they are built on top of Pragmatic Action Charts. In fact, both notations can be mixed arbitrarily to allow behavior trees to be called if the chart is currently in a specific location and vice versa, the chart can transfer control to another location as soon as a behavior tree finishes its execution.
Researchers have previously proposed augmenting Signal Temporal logic (STL) with the value freezing operator in order to express engineering properties that cannot be expressed in STL. This augmented logic is known as...
详细信息
ISBN:
(纸本)9798350378030;9798350378023
Researchers have previously proposed augmenting Signal Temporal logic (STL) with the value freezing operator in order to express engineering properties that cannot be expressed in STL. This augmented logic is known as STL*. The previous algorithms for STL* monitoring were intractable, and did not scale formulae with nested freeze variables. We present offline discrete-time monitoring algorithms with an acceleration heuristic, both for Boolean monitoring as well as for quantitative robustness monitoring. The acceleration heuristic operates over time intervals where subformulae hold true, rather than over the original trace sample-points. We present experimental validation of our algorithms, the results show that our algorithms can monitor over long traces for formulae with two or three nested freeze variables. Our work is the first work with monitoring algorithm implementations for STL* formulae with nested freeze variables.
Best practices of self-sovereign identity (SSI) are being intensively explored in academia and industry. Reusable solutions obtained from best practices are generalized as architectural patterns for systematic analysi...
详细信息
ISBN:
(纸本)9798350381993;9798350382006
Best practices of self-sovereign identity (SSI) are being intensively explored in academia and industry. Reusable solutions obtained from best practices are generalized as architectural patterns for systematic analysis and design reference, which significantly boosts productivity and increases the dependability of future implementations. For security-sensitive projects, architects make architectural decisions with careful consideration of security issues and solutions based on formal analysis and experiment results. In this paper, we propose a model-driven security analysis framework for analyzing architectural patterns of SSI systems with respect to a threat model built on our investigation of real-world security concerns. Our framework mechanizes a modeling language to formalize patterns and threats with security properties in temporal logic and automatically generates programs for verification via model checking. Besides, we present typical vulnerable patterns verified by SecureSSI, a standalone integrated development environment, integrating commonly used pattern and attacker models to practicalize our framework.
The proceedings contain 18 papers. The special focus in this conference is on programming Languages and Systems. The topics include: Random-Access Lists, from EE to FP;generic Reasoning of the Locally Namele...
ISBN:
(纸本)9789819789429
The proceedings contain 18 papers. The special focus in this conference is on programming Languages and Systems. The topics include: Random-Access Lists, from EE to FP;generic Reasoning of the Locally Nameless Representation;building a Correct-by-Construction Type Checker for a Dependently Typed Core Language;extending the Quantitative Pattern-Matching Paradigm;hybrid Verification of Declarative Programs with Arithmetic Non-fail Conditions;explaining Explanations in Probabilistic logicprogramming;quantum programming Without the Quantum Physics;quantum Bisimilarity Is a Congruence Under Physically Admissible Schedulers;non-deterministic, Probabilistic, and Quantum Effects Through the Lens of Event Structures;type-Based Verification of Connectivity Constraints in Lattice Surgery;on Computational Indistinguishability andlogical Relations;relative Completeness of Incorrectness Separation logic;OBRA: Oracle-Based, Relational, Algorithmic Type Verification;a Formal Verification Framework for Tezos Smart Contracts Based on Symbolic Execution;mode-based Reduction from Validity Checking of Fixpoint logic Formulas to Test-Friendly Reachability Problem;efficiently Adapting Stateless Model Checking for C11/C++11 to Mixed-Size Accesses.
暂无评论