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

12th international Conference on Verified Software, VSTTE 2020, and 13th international workshop on Numerical Software Verification, NSV 2020

12th International Conference on Verified Software, VSTTE 20...

引用

12th international Conference on Verified Software, VSTTE 2020, and 13th international workshop on Numerical Software Verification, NSV 2020

ISBN: (纸本)9783030636173

the proceedings contain 14 papers. the special focus in this conference is on Verified Software. the topics include: An Efficient Floating-Point Bit-Blasting API for Verifying C Programs;rigorous Enclosure of Round-Off Errors in Floating-Point Computations;towards Numerical Assistants: Trust, Measurement, Community, and Generality for the Numerical Workbench;combining Zonotope Abstraction and constraint programming for Synthesizing Inductive Invariants;QPR Verify: A Static Analysis Tool for Embedded Software Based on Bounded Model Checking;Verified Translation Between Purely Functional and Imperative Domain Specific Languages in HELIX;automatic Detection and Repair of Transition- Based Leakage in Software Binaries;BanditFuzz: A Reinforcement-Learning Based Performance Fuzzer for SMT Solvers;synthesis of Solar Photovoltaic Systems: Optimal Sizing Comparison;verified Transformations and Hoare logic: Beautiful Proofs for Ugly Assembly Language;MCBAT: Model Counting for constraints over Bounded Integer Arrays;Verification of an Optimized NTT Algorithm;vstte 2020 preface.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Automatic Generation of Test-cases of Increasing Complexity for Autonomous Vehicles at Intersections 13

Automatic Generation of Test-cases of Increasing Complexity ...

引用

13th ACM/IEEE international Conference on Cyber-Physical Systems (ICCPS )

作者： Karimi, Abolfazl Duggirala, Parasara Sridhar Univ N Carolina Chapel Hill NC 27515 USA

ISBN: (纸本)9781665409674

this paper presents a new framework for generating test-case scenarios for autonomous vehicles. We address two challenges in automatic test-case generation: first, a formal notion of test-case complexity, and second, an algorithm to generate more-complex test-cases. We characterize the complexity of a test-case by its set of solutions, and compare two complexities by the subset relation. the novelty of our definition is that it only relies on the pass-fail criteria of the test-case, rather than indirect or subjective assessments of what may challenge an ego vehicle to pass a test-case. Given a testcase, we model the problem of generating a more complex test-case as a constraint-satisfaction search problem. the search variables are the changes to the given test-case, and the search constraints define a solution to the search problem. the constraints include steering geometry of cars, the geometry of lanes, the shape of cars, traffic rules, bounds on longitudinal acceleration of cars, etc. To conquer the computational challenge, we divide the constraints to three categories and satisfy them with simulation, answer set programming, and SMT solving. We have implemented our algorithm using the Scenic libraries and the CARLA simulator and generate test-cases for several 3-way and 4-way intersections with different topologies. Our experiments demonstrate that both CARLA's autopilot and autopilot-plus-RSS (Responsibility-Sensitive Safety) can fail as the complexity of test-cases increase.

关键词： test-case complexity test-case generation traffic rules logic programming Answer Set programming Bezier curves SMT CARLA Scenic

来源：评论

学校读者我要写书评

暂无评论

RPO constraint solving is in NP 12th

引用

12th international workshop on Computer Science logic, CSL 1998 held as the annual Conference of the European Association for Computer Science logic, EACSL 1998

作者： Narendran, Paliath Rusinowitch, Michael Verma, Rakesh Institute of Programming and Logics Department of Computer Science State University of New York at Albany AlbanyNY12222 United States LORIA 615 rue du jardin botanique BP 101 Villers les Nancy cedex54602 France Dept. of Comp. Science University of Houston HoustonTX77204 United States

ISBN: (纸本)3540659226

A new decision procedure for the existential fragment of ordering constraints expressed using the recursive path ordering is presented. this procedure is nondeterministic and checks whether a set of constraints is solvable over the given signature, i.e., the signature over which the terms in the constraints are defined. It is shown that this non-deterministic procedure runs in polynomial time, thus establishing the membership of this problem in the complexity class NP for the first time. © Springer-Verlag Berlin Heidelberg 1999.

关键词： Polynomial approximation

来源：评论

学校读者我要写书评

暂无评论

Bipolar preference problems: Framework, properties and solving techniques

Bipolar preference problems: Framework, properties and solvi...

引用

11th annual European Research Consortium for Informatics and Mathematics (ERCIM) international workshop on constraint solving and constraint logic programming, CSCLP 2006

作者： S., Bistarelli M.S., Pini F., Rossi K.B., Venable Dipartimento di Scienze Università G. d'Annunzio Pescara Italy Istituto di Informatica e Telematica CNR Pisa Italy Dipartimento di Matematica Pura ed Applicata Università di Padova Italy

ISBN: (纸本)9783540738169

Real-life problems present several kinds of preferences. We focus on problems with both positive and negative preferences, that we call bipolar preference problems. Although seemingly specular notions, these two kinds of preferences should be dealt with differently to obtain the desired natural behaviour. We technically address this by generalizing the soft constraint formalism, which is able to model problems with one kind of preferences. We show that soft constraints model only negative preferences, and we define a new mathematical structure which allows to handle positive preferences as well. We also address the issue of the compensation between positive and negative preferences, studying the properties of this operation. Finally, we extend the notion of arc consistency to bipolar problems, and we show how branch and bound (with or without constraint propagation) can be easily adapted to solve such problems. © Springer-Verlag Berlin Heidelberg 2007.

关键词： Problem solving

来源：评论

学校读者我要写书评

暂无评论

On constraint satisfaction problems below P

On constraint satisfaction problems below P

引用

25th international workshop on Computer Science logic, CSL 2011/20th annual Conference of the European Association for Computer Science logic, EACSL

作者： Egri, László School of Computer Science McGill University Montreal Canada

ISBN: (纸本)9783939897323

Symmetric Datalog, a fragment of the logic programming language Datalog, is conjectured to capture all constraint satisfaction problems (CSP) in logarithmic space [10]. therefore developing tools that help us understand whether or not a CSP can be defined in symmetric Datalog is an important task. A simple, well-known fact is that for any CSP, a fixed set of structures O (an obstruction set) can be defined such that a CSP instance I is a yes-instance iff no structure in O maps homomorphically to I. A CSP having X-duality means that the set O can be chosen to have property X. It is widely known that a CSP is definable in Datalog and linear Datalog iff that CSP has bounded treewidth [12] and bounded pathwidth duality [6], respectively. In the case of symmetric Datalog, Bulatov, Krokhin and Larose ask for such a duality in [4]. We provide two such dualities, and we give applications. In particular, we give a short and simple new proof of the main result of [8] that "Maltsev + Datalog ⇒ symmetric Datalog". In the second part of the paper, we provide some evidence for the conjecture that every CSP in nondeterministic logarithmic space (NL) is definable in the Datalog fragment linear Datalog [6]. We recall that every problem in NL can be defined by a linear Datalog program with negation and access to an order over the domain of its input (linDat(suc,¬)) [6, 13, 15], or by a poly-size family of nondeterministic branching programs [20]. We consider the following restrictions of the previous models: read-once linDat(suc) (1-linDat(suc)), and monotone readonce nondeterministic branching programs (mnBP1). Although restricted, these models can still define NL-complete problems such as directed st-CONNECTIVITY, and also nontrivial problems in NL which are not definable in linear Datalog. We show that any CSP definable by a 1-linDat(suc) program or by a poly-size family of mnBP1s can also be defined by a linear Datalog program. It also follows that a wide class of CSPs-CSPs which

关键词： constraint satisfaction problems

来源：评论

学校读者我要写书评

暂无评论

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics): Preface

Lecture Notes in Computer Science (including subseries Lectu...

引用

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 2011年 6384 LNAI卷

作者： Larrosa, Javier O'Sullivan, Barry Technical University of Catalonia Department of Software C. Jordi Girona 1-3 08034 Barcelona Spain University College Cork Cork Constraint Computation Centre Western Road Cork Ireland

来源：评论

学校读者我要写书评

暂无评论

ASP-DPOP: solving Distributed constraint Optimization Problems with logic programming 14

ASP-DPOP: Solving Distributed Constraint Optimization Proble...

引用

international Conference on Autonomous Agents and Multiagent Systems

作者： Tiep Le Tran Cao Son Enrico Pontelli William Yeoh Department of Computer Science New Mexico State University

ISBN: (纸本)9781634391313

Researchers have used Distributed constraint Optimization Problems (DCOPs) to model various multi-agent coordination and resource allocation problems. However, existing DCOP algorithms have focused almost exclusively on imperative programming techniques. this paper explores a new direction, which is to develop algorithms that use declarative programming, specifically logic programming, techniques.

关键词： DCOP ASP Constrained optimization logic programming algorithms Resource utilization Distribute Declarative programming programming TECHNIQUES

来源：评论

学校读者我要写书评

暂无评论

Identification of labeled Time Petri nets

Identification of labeled Time Petri nets

引用

international workshop on Discrete Event Systems, WODES

作者： Francesco Basile Pasquale Chiacchio Jolanda Coppola Dip. Ingegneria dell'Informazione Ingegneria elettrica e Matematica applicata Univ. di Salerno Italy

In a previous paper we presented an approach to identify a Time Petri net system, given a set of observed timed sequences. the set of transitions, which coincides with the set of events, is assumed to be known, while the net structure, the initial marking and the firing duration of transitions are computed in one stage solving a mixed-integer linear programming problem derived from a set of logical predicates. In this paper we extend this approach by allowing that two transitions may share the same event label. then, the identified model is a labeled Time Petri net system. the identification problem can still be solved via a mixed-integer linear programming problem but the constraint set previously determined is modified.

关键词： Petri nets Timing Labeling Elevators Upper bound Structural rings Mixed integer linear programming

来源：评论

学校读者我要写书评

暂无评论

Average time complexity of the SAT1.2 algorithm 5th

Average time complexity of the SAT1.2 algorithm

引用

5th annual international Symposium on Algorithms and Computation, ISAAC 1994

作者： Gu, Jun Gu, Qian-Ping Dept. of Electrical and Computer Engineering Univ. of Calgary CalgaryABT2N 1N4 Canada Dept. of Computer Software The Univ. of Aizu Aizu-WakamatsuFukushima965-80 Japan

ISBN: (纸本)9783540583257

In this paper, we give an efficient algorithm, the SAT1.2 algorithm, for the SAT problem. For randomly generated formulas with n clauses, m variables, and l literals per clause, the average run time of the SAT1.2 algorithm is O(mO(1) n2) for l > 3 and n/m l/l, where α m are the solutions of the problem. thus, a random exhaustive search can efficiently solve the problem. the SAT1.2 algorithm can find a solution for a satisfiable CNF formula efficiently but gives an answer in 0(mO(1) 2m) time to an unsatisfiable CNF formula3. © 1994, Springer Verlag. All rights reserved.

关键词： Problem solving

来源：评论

学校读者我要写书评

暂无评论

Validating objected-oriented prototype of real-time systems with timed automata

Validating objected-oriented prototype of real-time systems ...

引用

international workshop on Rapid System Prototyping (RSP)

作者： Guoqiang Shu Chao Li Qing Wang Mingshu Li Institute of Software Chinese Academy and Sciences China

ISBN: (纸本)076951703X

Object-oriented development of real-time systems is becoming more and more prevalent. Unified Modeling Language (UML) is a standardized notation for describing object-oriented software design. While using UML to specify real-time systems, the formal validation of certain timing constraints becomes critical for the success of object-oriented development of real-time systems. Current development methods of real-time systems have not provided consistent support for verifying UML models of real-time systems. this paper presents a formal specification & validation method, FORTS, for object-oriented real-time system development using UML. the method presents a real-time extension of UML; describes the formal semantics of the UML extension; provides automatic transformation of UML models into timed automata; and verifies timing assertions presented by UML sequence diagram using model checking and the constraint solving technique. With tool support, FORTS conceals the complicated details of formal validation for users, thus providing the benefits of formal methods without bringing additional burden. A case study is presented at the end of the paper.

关键词： Prototypes Real time systems Automata Unified modeling language Object oriented modeling Timing Formal verification Chaos logic Software prototyping

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：