1,720,983 research outputs found
Guida alla programmazione in linguaggio C. Volume I: Fondamenti di programmazione
No full textLa seconda edizione presenta un aggiornamento dei contenuti allo scopo di rendere il testo più fedele ai programmi dei corsi di informatica di base del Politecnico di Torino così come strutturati recentemente. Questo ha comportato: 1. L'eliminazione degli argomenti relativi alla gestione dinamica della memoria, non più trattata nei corsi del primo anno. 2. L'eliminazione di alcuni esercizi di maggiore difficoltà logica. 3. La creazione, in ogni capitolo, di una sezione di esercizi proposti che estendono quelli precedentemente risolti e costituiscono un'ottima base per un approccio autonomo al "problem solving". La soluzione di tutti gli esercizi, tanto quelli "risolti" (la cui soluzione è già presentata nel testo), quanto quelli "proposti", è inclusa nel materiale elettronico associato al volume. Tale materiale, invece di essere fornito su CD, come nella versione precedente, è reso disponibile tramite il sito WEB dell'editor
Improving SAT-based Bounded Model Checking by Means of BDD-based Approximate Traversals
No full textBinary Decision Diagrams (BDDs) have been widely used in synthesis and verification.
Boolean Satisfiability (SAT) Solvers, on the other hand, have been gaining ground only recently, with the introduction of efficient implementation procedures.
Specifically, while BDDs have been mainly adopted to formally verify the correctness of hardware devices, SAT-based Bounded Model Checking (BMC) has been widely used for debugging.
In this paper, we combine BDD and SAT-based methods to increase the efficiency of BMC.
We first exploit affordable BDD-based symbolic approximate reachability analysis to gather information on the state space.
Then, we use the collected overestimated reachable state sets to restrict the search space of a SAT-based BMC.
This is possible by feeding the SAT solver with a description that is the combination of the original BMC problem with the extra information coming from BDD-based symbolic analysis.
We develop specific strategies to appropriately mix BDD and SAT efforts, and to efficiently convert BDD-based symbolic state set representations into SAT-oriented ones.
Experimental results prove the validity of our strategy to reduce the amount of variable assignments and variable conflicts generated by SAT solvers, with a subsequent significant performance gain.
We gather results with four among the most used SAT solvers, namely Chaff, Limmat, BerkMin, and Siege.
We could reduce the number of conflicts up to more than 100x, and the verification time up to 30x
A Novel SAT-Based Approach to the Task Graph Cost-Optimal Scheduling Problem
Full text linkThe Task Graph Cost-Optimal Scheduling Problem consists in scheduling a certain number of interdependent tasks onto a set of heterogeneous processors (characterized by idle and running rates per time unit), minimizing the cost of the entire process. This paper provides a novel formulation for this scheduling puzzle, in which an optimal solution is computed through a sequence of Binate Covering Problems, hinged within a Bounded Model Checking paradigm. In this approach, each covering instance, providing a min-cost trace for a given schedule depth, can be solved with several strategies, resorting to Minimum-Cost Satisfiability solvers or Pseudo-Boolean Optimization tools. Unfortunately, all direct resolution methods show very low efficiency and scalability. As a consequence, we introduce a specialized method to solve the same sequence of problems, based on a traditional all-solution SAT solver. This approach follows the "circuit cofactoring" strategy, as it exploits a powerful technique to capture a large set of solutions for any new SAT counter-example. The overall method is completed with a branch-and-bound heuristic which evaluates lower and upper bounds of the schedule length, to reduce the state space that has to be visited. Our results show that the proposed strategy significantly improves the blind binate covering schema, and it outperforms general purpose state-of-the-art tool
Thread-based multi-engine model checking for multicore platforms
No full textThis article describes a multithreaded, portfolio-based approach to model checking, where multiple cores are exploited as the underlying computing framework to support concurrent execution of cooperative engines. We introduce a portfolio-based approach to model checking. Our portfolio is first driven by an approximate runtime predictor that provides a heuristic approximation to a perfect oracle and suggests which engines are more suitable for each verification instance. Scalability and robustness of the overall model-checking effort highly rely on a concurrent, multithreaded model of execution. Following similar approaches in related application fields, we dovetail data partitioning, focused on proving several properties in parallel, and engine partitioning, based on concurrent runs of different model-checking engines competing for completion of the same problem. We investigate concurrency not only to effectively exploit several available engines, which operate independently, but also to show that a cooperative effort is possible. In this case, we adopt a straightforward, light-weight, model of inter-engine communication and data sharing. We provide a detailed description of the ideas, algorithms, and experimental results obtained on the benchmarks from the Hardware Model Checking Competition suites (HWMCC'10 and HWMCC'11)
- …
