检索结果-内蒙古大学图书馆

34th European Symposium on programming, ESOP 2025, which was held as part of the International Joint Conferences on theory and practice of Software, ETAPS 2025

作者： Sextl, Florian Rogalewicz, Adam Vojnar, Tomáš Zuleger, Florian Faculty of Informatics Institute of Logic and Computation TU Wien Vienna Austria Faculty of Information Technology Brno University of Technology Brno Czech Republic Faculty of Informatics Masaryk University Brno Czech Republic

ISBN: (纸本)9783031911200

Biabduction-based shape analysis is a compositional verification and analysis technique that can prove memory safety in the presence of complex, linked data structures. Despite its usefulness, several open problems persist for this kind of analysis;two of which we address in this paper. On the one hand, the original analysis is path-sensitive but cannot combine safety requirements for related branches. This causes the analysis to require additional soundness checks and decreases the analysis’ precision. We extend the underlying symbolic execution and propose a framework for shared abduction where a common pre-condition is maintained for related computation branches. On the other hand, prior implementations lift loop acceleration methods from forward analysis to biabduction analysis by applying them separately on the pre- and post-condition, which can lead to imprecise or even unsound acceleration results that do not form a loop invariant. In contrast, we propose biabductive loop acceleration, which explicitly constructs and checks candidate loop invariants. For this, we also introduce a novel heuristic called shape extrapolation. This heuristic takes advantage of locality in the handling of list-like data structures (which are the most common data structures found in low-level code) and jointly accelerates pre- and post-conditions by extrapolating the related shapes. In addition to making the analysis more precise, our techniques also make biabductive analysis more efficient since they are sound in just one analysis phase. In contrast, prior techniques always require two phases (as the first phase can produce contracts that are unsound and must hence be verified). We experimentally confirm that our techniques improve on prior techniques;both in terms of precision and runtime of the analysis. © The Author(s) 2025.

关键词： Biabduction Shape Analysis

来源：评论

学校读者我要写书评

暂无评论

Towards Metric Temporal Answer Set programming

Towards Metric Temporal Answer Set Programming

引用

36th International Conference on logic programming (ICLP)

作者： Cabalar, Pedro Dieguez, Martin Schaub, Torsten Schuhmann, Anna Univ A Coruna La Coruna Spain Univ Angers LERIA Angers France Univ Potsdam Potsdam Germany

We elaborate upon the theoretical foundations of a metric temporal extension of Answer Set programming. In analogy to previous extensions of ASP with constructs from Linear Temporal and Dynamic logic, we accomplish this in the setting of the logic of Here-and-There and its non-monotonic extension, called Equilibrium logic. More precisely, we develop our logic on the same semantic underpinnings as its predecessors and thus use a simple time domain of bounded time steps. This allows us to compare all variants in a uniform framework and ultimately combine them in a common implementation.

关键词： Semantics

来源：评论

学校读者我要写书评

暂无评论

A General Framework for Stable Roommates Problems using Answer Set programming

引用

theory and practice of logic programming 2020年第6期20卷 911-925页

作者： ERDEM, E. S. R. A. FIDAN, M. U. G. E. MANLOVE, D. A. V. I. D. PROSSER, P. A. T. R. I. C. K. Sabanci Univ Fac Engn & Nat Sci Istanbul Turkey Univ Glasgow Sch Comp Sci Glasgow Lanark Scotland

The Stable Roommates problem (SR) is characterized by the preferences of agents over other agents as roommates: each agent ranks all others in strict order of preference. A solution to SR is then a partition of the agents into pairs so that each pair shares a room, and there is no pair of agents that would block this matching (i.e., who prefers the other to their roommate in the matching). There are interesting variations of SR that are motivated by applications (e.g., the preference lists may be incomplete (SRI) and involve ties (SRTI)), and that try to find a more fair solution (e.g., Egalitarian SR). Unlike the Stable Marriage problem, every SR instance is not guaranteed to have a solution. For that reason, there are also variations of SR that try to find a good-enough solution (e.g., Almost SR). Most of these variations are NP-hard. We introduce a formal framework, called SRTI-ASP, utilizing the logic programming paradigm Answer Set programming, that is provable and general enough to solve many of such variations of SR. Our empirical analysis shows that SRTI-ASP is also promising for applications.

关键词： stable roommates problem answer set programming declarative problem solving

来源：评论

学校读者我要写书评

暂无评论

Modular Answer Set programming as a Formal Specification Language

引用

theory and practice of logic programming 2020年第5期20卷 767-782页

作者： Cabalar, Pedro Fandinno, Jorge Lierler, Yuliya Univ A Coruna La Coruna Spain Univ Potsdam Potsdam Germany Univ Nebraska Omaha Omaha NE USA

In this paper, we study the problem of formal verification for Answer Set programming (ASP), namely, obtaining aformal proofshowing that the answer sets of a given (non-ground) logic programPcorrectly correspond to the solutions to the problem encoded byP, regardless of the problem instance. To this aim, we use a formal specification language based on ASP modules, so that each module can be proved to capture some informal aspect of the problem in an isolated way. This specification language relies on a novel definition of (possibly nested, first order)program modulesthat may incorporate local hidden atoms at different levels. Then,verifyingthe logic programPamounts to prove some kind of equivalence betweenPand its modular specification.

关键词： Answer Set programming Formal Specification Formal Verification Modular logic Programs

来源：评论

学校读者我要写书评

暂无评论

Swift Markov logic for Probabilistic Reasoning on Knowledge Graphs

arXiv

引用

arXiv 2022年

作者： Bellomarini, Luigi Laurenza, Eleonora Sallinger, Emanuel Sherkhonov, Evgeny Banca d'Italia Italy Tu Wien Austria University of Oxford United Kingdom

We provide a framework for probabilistic reasoning in Vadalog-based Knowledge Graphs (KGs), satisfying the requirements of ontological reasoning: full recursion, powerful existential quantification, expression of inductive definitions. Vadalog is a Knowledge Representation and Reasoning (KRR) language based on Warded Datalog+/-, a logical core language of existential rules, with a good balance between computational complexity and expressive power. Handling uncertainty is essential for reasoning with KGs. Yet Vadalog andWarded Datalog+/- are not covered by the existing probabilistic logic programming and statistical relational learning approaches for several reasons, including insufficient support for recursion with existential quantification, and the impossibility to express inductive definitions. In this work, we introduce Soft Vadalog, a probabilistic extension to Vadalog, satisfying these desiderata. A Soft Vadalog program induces what we call a Probabilistic Knowledge Graph (PKG), which consists of a probability distribution on a network of chase instances, structures obtained by grounding the rules over a database using the chase procedure. We exploit PKGs for probabilistic marginal inference. We discuss the theory and present MCMC-chase, a Monte Carlo method to use Soft Vadalog in practice. We apply our framework to solve data management and industrial problems, and experimentally evaluate it in the Vadalog system. Under consideration in theory and practice of logic programming (TPLP). © 2022, CC BY-NC-ND.

关键词： Markov processes

来源：评论

学校读者我要写书评

暂无评论

IASCAR: Incremental Answer Set Counting by Anytime Refinement

arXiv

引用

arXiv 2023年

作者： Fichte, Johannes K. Gaggl, Sarah Alice Hecher, Markus Rusovac, Dominik Sweden TU Dresden Logic Programming and Argumentation Group Germany Massachusetts Institute of Technology United States

Answer set programming (ASP) is a popular declarative programming paradigm with various applications. Programs can easily have many answer sets that cannot be enumerated in practice, but counting still allows quantifying solution spaces. If one counts under assumptions on literals, one obtains a tool to comprehend parts of the solution space, so-called answer set navigation. However, navigating through parts of the solution space requires counting many times, which is expensive in theory. Knowledge compilation compiles instances into representations on which counting works in polynomial time. However, these techniques exist only for CNF formulas, and compiling ASP programs into CNF formulas can introduce an exponential overhead. This paper introduces a technique to iteratively count answer sets under assumptions on knowledge compilations of CNFs that encode supported models. Our anytime technique uses the inclusion-exclusion principle to improve bounds by over- and undercounting systematically. In a preliminary empirical analysis, we demonstrate promising results. After compiling the input (offline phase), our approach quickly (re)counts. Copyright © 2023, The Authors. All rights reserved.

关键词： Iterative methods

来源：评论

学校读者我要写书评

暂无评论

Polymorphic computation systems: theory and practice of confluence with call-by-value

引用

SCIENCE OF COMPUTER programming 2020年第0期187卷 102322-000页

作者： Hamana, Makoto Abe, Tatsuya Kikuchi, Kentaro Gunma Univ Dept Comp Sci Maebashi Gunma Japan Chiba Inst Technol STAIR Lab Narashino Chiba Japan Tohoku Univ Res Inst Elect Commun Sendai Miyagi Japan

We present a new framework of polymorphic computation rules that can accommodate a distinction between values and non-values. It is suitable for analysing fundamental calculi of programming languages. We develop a type inference algorithm and new criteria to check the confluence property. These techniques are then implemented in our automated confluence checking tool PolySOL. Its effectiveness is demonstrated through examination of various calculi, including the call-by-need lambda-calculus, Moggi's computational lambdacalculus, and skew-monoidal categories. (C) 2019 Elsevier B.V. All rights reserved.

关键词： Polymorphism lambda-calculus Type inference Second-order algebraic theory Confluence

来源：评论

学校读者我要写书评

暂无评论

24th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2021 held as part of the European Joint Conferences on theory and practice of Software, ETAPS 2021

24th International Conference on Foundations of Software Sci...

引用

24th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2021 held as part of the European Joint Conferences on theory and practice of Software, ETAPS 2021

ISBN: (纸本)9783030719944

The proceedings contain 28 papers. The special focus in this conference is on Foundations of Software Science and Computation Structures. The topics include: Finding cut-offs in leaderless rendez-vous protocols is easy;fixpoint theory – upside down;"Most of" leads to undecidability: Failure of adding frequencies to LTL;combining semilattices and semimodules;one-way resynchronizability of word transducers;fair refinement for asynchronous session types;running time analysis of broadcast consensus protocols;leafy automata for higher-order concurrency;factorization in call-by-name and call-by-value calculi via linear logic;generalized bounded linear logic and its categorical semantics;focused proof-search in the logic of bunched implications;interpolation and amalgamation for arrays with maxdiff;adjoint reactive gui programming;on the expressiveness of büchi arithmetic;learning pomset automata;parametricity for primitive nested types;the spirit of node replication;nondeterministic and co-nondeterministic implies deterministic, for data languages;certifying inexpressibility;a general semantic construction of dependent refinement type systems, categorically;simple stochastic games with almost-sure energy-parity objectives are in np and conp;nondeterministic syntactic complexity;a string diagrammatic axiomatisation of finite-state automata;work-sensitive dynamic complexity of formal languages;the structure of sum-over-paths, its consequences, and completeness for clifford;a quantified coalgebraic van benthem theorem.

关键词：

来源：评论

学校读者我要写书评

暂无评论

An Automated Deductive Verification Framework for Circuit-building Quantum Programs 1

引用

30th European Symposium on programming (ESOP) Held as Part of the 24th European Joint Conferences on theory and practice of Software (ETAPS)

作者： Chareton, Christophe Bardin, Sebastien Bobot, Francois Perrelle, Valentin Valiron, Benoit Univ Paris Saclay Cent Supelec LMF Gif Sur Yvette France Univ Paris Saclay LIST CEA Palaiseau France

ISBN: (数字)9783030720193

ISBN: (纸本)9783030720193;9783030720186

While recent progress in quantum hardware open the door for significant speedup in certain key areas, quantum algorithms are still hard to implement right, and the validation of such quantum programs is a challenge. In this paper we propose QBRICKS, a formal verification environment for circuit-building quantum programs, featuring both parametric specifications and a high degree of proof automation. We propose a logical framework based on first-order logic, and develop the main tool we rely upon for achieving the automation of proofs of quantum specification: PPS, a parametric extension of the recently developed path sum semantics. To back-up our claims, we implement and verify parametric versions of several famous and non-trivial quantum algorithms, including the quantum parts of Shor's integer factoring, quantum phase estimation (QPE) and Grover's search.

关键词： deductive verification quantum programming quantum circuits

来源：评论

学校读者我要写书评

暂无评论

Optimizing the workload allocation in an e-fulfillment center using queueing theory

Optimizing the workload allocation in an e-fulfillment cente...

引用

作者： Leijnse, Nikki University of Twente

学位级别：硕士

In this study, we propose an approach to release pick batches to the warehouse of an e-fulfillment center, that takes into account the workload throughout the entire process. This approach is based on methods from queueing theory and involves some linear programming as well. In order to investigate whether the proposed approach performs better than the current approach, a mathematical model is formulated and for validation purposes a simulation model was created as well. The performance of the current and the proposed approach are assessed on the average throughput, sojourn time and work in progress. The results of the simulation model show that, with a significance level of 1%, the proposed approach performs significantly better than the current approach. However, the formulated mathematical model turns out to capture the logic behind the processes in the warehouse insufficiently enough to accurately determine the performance measures. Further research is required to adjust the mathematical model such that the gap between the model and practice becomes smaller.

关键词：

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：