Zobrazeno 1 - 10
of 52
pro vyhledávání: '"Tommi Junttila"'
Publikováno v:
Logical Methods in Computer Science, Vol Volume 2, Issue 5 (2006)
We consider the problem of bounded model checking (BMC) for linear temporal logic (LTL). We present several efficient encodings that have size linear in the bound. Furthermore, we show how the encodings can be extended to LTL with past operators (PLT
Externí odkaz:
https://doaj.org/article/ba6ba9628bbc4efb911d114cf78641d5
Autor:
Massimo Bartoletti, James Chiang, Tommi Junttila, Alberto Lluch Lafuente, Massimiliano Mirelli, Andrea Vandin
Publikováno v:
Leveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning ISBN: 9783031197581
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::4d218e5ef9e58ad427be40e69bc39cab
https://doi.org/10.1007/978-3-031-19759-8_21
https://doi.org/10.1007/978-3-031-19759-8_21
Publikováno v:
Frontiers in Artificial Intelligence and Applications
When studying the propositional satisfiability problem (SAT), that is, the problem of deciding whether a propositional formula is satisfiable, it is typically assumed that the formula is given in the conjunctive normal form (CNF). Also most software
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::d47391638fd76bc97b8581c4bc213d52
https://doi.org/10.3233/faia201011
https://doi.org/10.3233/faia201011
This paper presents a technique for symmetry reduction that adaptively assigns a prefix of variables in a system of constraints so that the generated prefix-assignments are pairwise nonisomorphic under the action of the symmetry group of the system.
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::dbcab1470b10ecd0676b7c3e18a28176
Publikováno v:
Science of Computer Programming. 77:1095-1121
This paper discusses bounded model checking (BMC) for asynchronous systems. Bounded model checking is a technique that employs the power of efficient SAT and SMT solvers for model checking. The main contribution of this paper is the presentation of a
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::d7d8e103c12b3670396fe06cd8608620
https://doi.org/10.1016/j.scico.2011.07.005
https://doi.org/10.1016/j.scico.2011.07.005
Publikováno v:
Fundamenta Informaticae. 107:289-311
This paper studies the following question: given an instance of the propositional satisfiability problem, a randomized satisfiability solver, and a cluster of n computers, what is the best way to use the computers to solve the instance? Two approache
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::1429b18bb0c83e1f60c7271fbdcba3ba
https://doi.org/10.3233/fi-2011-404
https://doi.org/10.3233/fi-2011-404
Publikováno v:
Journal on Satisfiability, Boolean Modeling and Computation. 6:223-244
Computational Grids provide a widely distributed computing environment suitable for randomized SAT solving. This paper develops techniques for incorporating clause learning, known to yield significant speed-ups in the sequential case, in such a distr
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::4cadf197878d2ce3eee8b2a389d6546b
https://doi.org/10.3233/sat190069
https://doi.org/10.3233/sat190069
Autor:
Matti Järvisalo, Tommi Junttila
Publikováno v:
Constraints. 14:325-356
The techniques for making decisions, that is, branching, play a central role in complete methods for solving structured instances of constraint satisfaction problems (CSPs). In this work we consider branching heuristics in the context of propositiona
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::62bd7b97031bd7ca8b43451d2b4053e1
https://doi.org/10.1007/s10601-008-9062-z
https://doi.org/10.1007/s10601-008-9062-z
Autor:
Silvio Ranise, Roberto Bruttomesso, Roberto Sebastiani, Tommi Junttila, Alessandro Cimatti, Marco Bozzano, Peter van Rossum
Publikováno v:
Information and Computation, 10, 10, pp. 1493-2525
Information and Computation, 10, 1493-2525
Information and Computation, 10, 1493-2525
Many approaches to deciding the satisfiability of quantifier-free formulae with respect to a background theory T—also known as Satisfiability Modulo Theory, or SMT(T)—rely on the integration between an enumerator of truth assignments and a decisi
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::816d9ca4e9134bb295baef145f7f8283
https://doi.org/10.1016/j.ic.2005.05.011
https://doi.org/10.1016/j.ic.2005.05.011
Autor:
Roberto Sebastiani, Stephan Schulz, Tommi Junttila, Roberto Bruttomesso, Alessandro Cimatti, Peter van Rossum, Marco Bozzano
Publikováno v:
Journal of Automated Reasoning. 35:265-293
Recent improvements in propositional satisfiability techniques (SAT) made it possible to tackle successfully some hard real-world problems (e.g., model-checking, circuit testing, propositional planning) by encoding into SAT. However, a purely Boolean
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::b8df01685fb6273b56b5de308039f5bc
https://doi.org/10.1007/s10817-005-9004-z
https://doi.org/10.1007/s10817-005-9004-z