Forest logic Programs (FoLP) are a decidable fragment of Open Answer Set programming (OASP) which have the forest model property. OASP extends Answer Set programming (ASP) with open domains—a feature which makes it p...
详细信息
logic programs with graded modality (LPGMs) combine ideas underlying graded modal logic and answer set programming. logicprogramming under answer set semantics is extended with a new graded modality M[lb:ub] where lb...
详细信息
Recently, there has been an increase of reported security threats hitting organizations. Some of them are originated from the assignments to users of inappropriate permissions on organizational sensitive data. thus it...
详细信息
ISBN:
(纸本)9780769545356
Recently, there has been an increase of reported security threats hitting organizations. Some of them are originated from the assignments to users of inappropriate permissions on organizational sensitive data. thus it is crucial for organizations to recognize as early as possible the risks deriving by inappropriate access right management and to identify the solutions that they need to prevent such risks. In this paper, we propose a framework to identify threats during the requirements analysis of organizations' IT systems. With respect to other works which have attempted to include security analysis into requirement engineering process (e.g., KAOS, Elahi et al., Asnar et al.), our framework does not rely on the level of expertise of the security analyst to detect threats but allows to automatically identify threats that derive from inappropriate access management. To capture the organization's setting and the system stakeholders' requirements, we adopt SI* [1], a requirement engineering framework founded on the concepts of actors, goals, tasks and resources. this framework extends SI* with a reasoning technique that identifies potential security threats on resources and relevant goals. the reasoning is based on Answer Set programming ( ASP) logic rules that take into account the relationships between resources and the delegation of permission relations between actors. We illustrate this framework using an eHealth scenario.
this work makes an overview on an hybrid formalism that combines the syntax of Linear-time Temporal logic (LTL) with a nonmonotonic selection of models based on Equilibrium logic. the resulting approach, called Tempor...
详细信息
Hand-optimized assembly language code is often difficult to formally verify. this paper combines Hoare logic with verified code transformations to make it easier to verify such code. this approach greatly simplifies e...
详细信息
ISBN:
(纸本)9783030636173;9783030636180
Hand-optimized assembly language code is often difficult to formally verify. this paper combines Hoare logic with verified code transformations to make it easier to verify such code. this approach greatly simplifies existing proofs of highly optimized OpenSSL-based AES-GCM cryptographic code. Furthermore, applying various verified transformations to the AES-GCM code enables additional platform-specific performance improvements.
We propose to extend an existing framework combining abstract interpretation and continuous constraint programming for numerical invariant synthesis, by using more expressive underlying abstract domains, such as zonot...
详细信息
ISBN:
(纸本)9783030636173;9783030636180
We propose to extend an existing framework combining abstract interpretation and continuous constraint programming for numerical invariant synthesis, by using more expressive underlying abstract domains, such as zonotopes. the original method, which relies on iterative refinement, splitting and tightening a collection of abstract elements until reaching an inductive set, was initially presented in combination with simple underlying abstract elements: boxes and octagons. the novelty of our work is to use zonotopes, a sub-polyhedric domain that shows a good compromise between cost and precision. As zonotopes are not closed under intersection, we had to extend the existing framework, in addition to designing new operations on zonotopes, such as a novel splitting algorithm based on paving zonotopes by sub-zonotopes and parallelotopes. We implemented this method on top of the APRON library, and tested it on programs with non-linear loops that present complex, possibly non-convex, invariants. We present some results demonstrating boththe interest of this splitting-based algorithm to synthesize invariants on such programs, and the good compromise presented by its use in combination with zonotopes with respect to its use with both simpler domains such as boxes and octagons, and more expressive domains such as polyhedra.
the proceedings contain 17 papers. the special focus in this conference is on Reversible Computation. the topics include: A Tangled Web of 12 Lens Laws;splitting Recursion Schemes into Reversible and Classical Interac...
ISBN:
(纸本)9783030798369
the proceedings contain 17 papers. the special focus in this conference is on Reversible Computation. the topics include: A Tangled Web of 12 Lens Laws;splitting Recursion Schemes into Reversible and Classical Interacting threads;reversibility of Executable Interval Temporal logic Specifications;efficient Construction of Functional Representations for Quantum Algorithms;Finding Optimal Implementations of Non-native CNOT Gates Using SAT;fast Swapping in a Quantum Multiplier Modelled as a Queuing Network;OR-Toffoli and OR-Peres Reversible Gates;variational Quantum Eigensolver and Its Applications;reversible Functional Array programming;Compiling Janus to RSSA;causal-Consistent Debugging of Distributed Erlang Programs;towards a Unified Language Architecture for Reversible Object-Oriented programming;Towards a Truly Concurrent Semantics for Reversible CCS;Forward-Reverse Observational Equivalences in CCSK;explicit Identifiers and Contexts in Reversible Concurrent Calculus.
We present a new approach to evaluate conditionals in human reasoning. this approach is based on the weak completion semantics which has been successfully applied to adequately model various other human reasoning task...
详细信息
Answer set programming is a programming paradigm where a given problem is formalized as a logic program whose answer sets correspond to the solutions to the problem. In this paper, we link answer set programming with ...
详细信息
the proceedings contain 29 papers. the special focus in this conference is on Integration of AI and OR Techniques in Constraint programming. the topics include: On CNF encodings of decision diagrams;time-series constr...
ISBN:
(纸本)9783319339535
the proceedings contain 29 papers. the special focus in this conference is on Integration of AI and OR Techniques in Constraint programming. the topics include: On CNF encodings of decision diagrams;time-series constraints: improvements and application in CP and MIP contexts;decomposition based on decision diagrams;logic-based decomposition methods for the travelling purchaser problem;lagrangian decomposition via sub-problem search;non-linear optimization of business models in the electricity market;weighted spanning tree constraint with explanations;application to an energy cost-aware production planning problem for tissue manufacturing;cyclic routing of unmanned aerial vehicles;parallelizing constraint programming with learning;parallel composition of scheduling solvers;rail capacity modelling with constraint programming;scheduling home hospice care withlogic-based benders decomposition;a global constraint for mining sequential patterns with GAP constraint;a reservoir balancing constraint with applications to bike-sharing;optimization models for a real-world snow plow routing problem;a stochastic continuous optimization backend for MiniZinc with applications to geometrical placement problems;balancing nursing workload by constraint programming;designing spacecraft command loops using two-dimension vehicle routing;constraint programming approach for spatial packaging problem;detecting semantic groups in MIP Models;revisiting two-sided stability constraints;optimal flood mitigation over flood propagation approximations;a bit-vector solver with word-level propagation;a new solver for the minimum weighted vertex cover problem and optimal upgrading schemes for effective shortest paths in networks.
暂无评论