Info
- Utilizzare la checkbox di selezione a fianco di ciascun documento per attivare le funzionalità di stampa, invio email, download nei formati disponibili del (i) record.
Computer Aided Verification [[electronic resource] ] : 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014, Proceedings / / edited by Armin Biere, Roderick Bloem
| Computer Aided Verification [[electronic resource] ] : 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014, Proceedings / / edited by Armin Biere, Roderick Bloem |
| Edizione | [1st ed. 2014.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2014 |
| Descrizione fisica | 1 online resource (XXXIV, 877 p. 205 illus.) |
| Disciplina | 005.1015113 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer science
Software engineering Machine theory Computer engineering Computer networks Computer Science Logic and Foundations of Programming Software Engineering Formal Languages and Automata Theory Computer Engineering and Networks |
| ISBN | 3-319-08867-X |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Software Verification -- The Spirit of Ghost Code -- SMT-Based Model Checking for Recursive Programs -- Property-Directed Shape Analysis -- Shape Analysis via Second-Order Bi-Abduction -- ICE: A Robust Framework for Learning Invariants -- From Invariant Checking to Invariant Inference Using Randomized Search -- SMACK: Decoupling Source Language Details from Verifier Implementations -- Security -- Synthesis of Masking Countermeasures against Side Channel Attacks -- Temporal Mode-Checking for Runtime Monitoring of Privacy Policies -- String Constraints for Verification -- A Conference Management System with Verified Document Confidentiality -- VAC - Verifier of Administrative Role-Based Access Control Policies -- Automata -- From LTL to Deterministic Automata: A Safraless Compositional Approach -- Symbolic Visibly Pushdown Automata -- Model Checking and Testing -- Engineering a Static Verification Tool for GPU Kernels -- Lazy Annotation Revisited -- Interpolating Property Directed Reachability -- Verifying Relative Error Bounds Using Symbolic Simulation -- Regression Test Selection for Distributed Software Histories -- GPU-Based Graph Decomposition into Strongly Connected and Maximal End Components -- Software Verification in the Google App-Engine Cloud -- The nuXmv Symbolic Model Checker -- Biology and Hybrid Systems Analyzing and Synthesizing Genomic Logic Functions -- Finding Instability in Biological Models -- Invariant Verification of Nonlinear Hybrid Automata Networks of Cardiac Cells -- Diamonds Are a Girl’s Best Friend: Partial Order Reduction for Timed Automata with Abstractions -- Reachability Analysis of Hybrid Systems Using Symbolic Orthogonal Projections -- Verifying LTL Properties of Hybrid Systems with K-Liveness -- Games and Synthesis -- Safraless Synthesis for Epistemic Temporal Specifications -- Minimizing Running Costs in Consumption Systems -- CEGAR for Qualitative Analysis of Probabilistic Systems -- Optimal Guard Synthesis for Memory Safety -- Don’t Sit on the Fence: A Static Analysis Approach to Automatic Fence Insertion -- MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications -- Solving Games without Controllable Predecessor -- G4LTL-ST: Automatic Generation of PLC Programs -- Concurrency -- Automatic Atomicity Verification for Clients of Concurrent Data Structures -- Regression-Free Synthesis for Concurrency -- Bounded Model Checking of Multi-threaded C Programs via Lazy Sequentialization -- An SMT-Based Approach to Coverability Analysis -- LEAP: A Tool for the Parametrized Verification of Concurrent Datatypes -- SMT and Theorem Proving -- Monadic Decomposition -- A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions -- Bit-Vector Rewriting with Automatic Rule Generation -- A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors -- AVATAR: The Architecture for First-Order Theorem Provers -- Automating Separation Logic with Trees and Data -- A Nonlinear Real Arithmetic Fragment -- Yices 2.2 -- Bounds and Termination -- A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis -- Symbolic Resource Bound Inference for Functional Programs -- Proving Non-termination Using Max-SMT -- Termination Analysis by Learning Terminating Programs -- Causal Termination of Multi-threaded Programs -- Abstraction -- Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR) -- Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath Abstraction -- QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers. |
| Record Nr. | UNISA-996199992703316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2014 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Computer Aided Verification : 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014, Proceedings / / edited by Armin Biere, Roderick Bloem
| Computer Aided Verification : 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014, Proceedings / / edited by Armin Biere, Roderick Bloem |
| Edizione | [1st ed. 2014.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2014 |
| Descrizione fisica | 1 online resource (XXXIV, 877 p. 205 illus.) |
| Disciplina | 005.1015113 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer science
Software engineering Machine theory Computer engineering Computer networks Computer Science Logic and Foundations of Programming Software Engineering Formal Languages and Automata Theory Computer Engineering and Networks |
| ISBN | 3-319-08867-X |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Software Verification -- The Spirit of Ghost Code -- SMT-Based Model Checking for Recursive Programs -- Property-Directed Shape Analysis -- Shape Analysis via Second-Order Bi-Abduction -- ICE: A Robust Framework for Learning Invariants -- From Invariant Checking to Invariant Inference Using Randomized Search -- SMACK: Decoupling Source Language Details from Verifier Implementations -- Security -- Synthesis of Masking Countermeasures against Side Channel Attacks -- Temporal Mode-Checking for Runtime Monitoring of Privacy Policies -- String Constraints for Verification -- A Conference Management System with Verified Document Confidentiality -- VAC - Verifier of Administrative Role-Based Access Control Policies -- Automata -- From LTL to Deterministic Automata: A Safraless Compositional Approach -- Symbolic Visibly Pushdown Automata -- Model Checking and Testing -- Engineering a Static Verification Tool for GPU Kernels -- Lazy Annotation Revisited -- Interpolating Property Directed Reachability -- Verifying Relative Error Bounds Using Symbolic Simulation -- Regression Test Selection for Distributed Software Histories -- GPU-Based Graph Decomposition into Strongly Connected and Maximal End Components -- Software Verification in the Google App-Engine Cloud -- The nuXmv Symbolic Model Checker -- Biology and Hybrid Systems Analyzing and Synthesizing Genomic Logic Functions -- Finding Instability in Biological Models -- Invariant Verification of Nonlinear Hybrid Automata Networks of Cardiac Cells -- Diamonds Are a Girl’s Best Friend: Partial Order Reduction for Timed Automata with Abstractions -- Reachability Analysis of Hybrid Systems Using Symbolic Orthogonal Projections -- Verifying LTL Properties of Hybrid Systems with K-Liveness -- Games and Synthesis -- Safraless Synthesis for Epistemic Temporal Specifications -- Minimizing Running Costs in Consumption Systems -- CEGAR for Qualitative Analysis of Probabilistic Systems -- Optimal Guard Synthesis for Memory Safety -- Don’t Sit on the Fence: A Static Analysis Approach to Automatic Fence Insertion -- MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications -- Solving Games without Controllable Predecessor -- G4LTL-ST: Automatic Generation of PLC Programs -- Concurrency -- Automatic Atomicity Verification for Clients of Concurrent Data Structures -- Regression-Free Synthesis for Concurrency -- Bounded Model Checking of Multi-threaded C Programs via Lazy Sequentialization -- An SMT-Based Approach to Coverability Analysis -- LEAP: A Tool for the Parametrized Verification of Concurrent Datatypes -- SMT and Theorem Proving -- Monadic Decomposition -- A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions -- Bit-Vector Rewriting with Automatic Rule Generation -- A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors -- AVATAR: The Architecture for First-Order Theorem Provers -- Automating Separation Logic with Trees and Data -- A Nonlinear Real Arithmetic Fragment -- Yices 2.2 -- Bounds and Termination -- A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis -- Symbolic Resource Bound Inference for Functional Programs -- Proving Non-termination Using Max-SMT -- Termination Analysis by Learning Terminating Programs -- Causal Termination of Multi-threaded Programs -- Abstraction -- Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR) -- Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath Abstraction -- QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers. |
| Record Nr. | UNINA-9910484370003321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2014 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Handbook of satisfiability [[electronic resource] /] / edited by Armin Biere ... [et al.]
| Handbook of satisfiability [[electronic resource] /] / edited by Armin Biere ... [et al.] |
| Pubbl/distr/stampa | Amsterdam, The Netherlands ; ; Washington, DC, : IOS Press, c2009 |
| Descrizione fisica | 1 online resource (980 p.) |
| Disciplina | 006.3 |
| Altri autori (Persone) | BiereArmin |
| Collana | Frontiers in artificial intelligence and applications |
| Soggetto topico |
Propositional calculus
Decision making Computer algorithms Algebra, Boolean |
| Soggetto genere / forma | Electronic books. |
| ISBN |
1-4416-1678-0
1-60750-376-X 600-00-1439-2 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Title page; Contents; Part I. Theory and Algorithms; Chapter 1. A History of Satisfiability; Chapter 2. CNF Encodings; Chapter 3. Complete Algorithms; Chapter 4. CDCL Solvers; Chapter 5. Look-Ahead Based SAT Solvers; Chapter 6. Incomplete Algorithms; Chapter 7. Fundaments of Branching Heuristics; Chapter 8. Random Satisfiability; Chapter 9. Exploiting Runtime Variation in Complete Solvers; Chapter 10. Symmetry and Satisfiability; Chapter 11. Minimal Unsatisfiability and Autarkies; Chapter 12. Worst-Case Upper Bounds; Chapter 13. Fixed-Parameter Tractability
Part II. Applications and ExtensionsChapter 14. Bounded Model Checking; Chapter 15. Planning and SAT; Chapter 16. Software Verification; Chapter 17. Combinatorial Designs by SAT Solvers; Chapter 18. Connections to Statistical Physics; Chapter 19. MaxSAT; Chapter 20. Model Counting; Chapter 21. Non-Clausal SAT and ATPG; Chapter 22. Pseudo-Boolean and Cardinality Constraints; Chapter 23. QBF Theory; Chapter 24. QBFs reasoning; Chapter 25. SAT Techniques for Modal and Description Logics; Chapter 26. Satisfiability Modulo Theories; Chapter 27. Stochastic Boolean Satisfiability; Subject Index Cited Author IndexContributing Authors and Affiliations |
| Record Nr. | UNINA-9910455344403321 |
| Amsterdam, The Netherlands ; ; Washington, DC, : IOS Press, c2009 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Handbook of satisfiability [[electronic resource] /] / edited by Armin Biere ... [et al.]
| Handbook of satisfiability [[electronic resource] /] / edited by Armin Biere ... [et al.] |
| Pubbl/distr/stampa | Amsterdam, The Netherlands ; ; Washington, DC, : IOS Press, c2009 |
| Descrizione fisica | 1 online resource (980 p.) |
| Disciplina | 006.3 |
| Altri autori (Persone) | BiereArmin |
| Collana | Frontiers in artificial intelligence and applications |
| Soggetto topico |
Propositional calculus
Decision making Computer algorithms Algebra, Boolean |
| ISBN |
1-4416-1678-0
1-60750-376-X 600-00-1439-2 |
| Classificazione |
ST 125
ST 300 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Title page; Contents; Part I. Theory and Algorithms; Chapter 1. A History of Satisfiability; Chapter 2. CNF Encodings; Chapter 3. Complete Algorithms; Chapter 4. CDCL Solvers; Chapter 5. Look-Ahead Based SAT Solvers; Chapter 6. Incomplete Algorithms; Chapter 7. Fundaments of Branching Heuristics; Chapter 8. Random Satisfiability; Chapter 9. Exploiting Runtime Variation in Complete Solvers; Chapter 10. Symmetry and Satisfiability; Chapter 11. Minimal Unsatisfiability and Autarkies; Chapter 12. Worst-Case Upper Bounds; Chapter 13. Fixed-Parameter Tractability
Part II. Applications and ExtensionsChapter 14. Bounded Model Checking; Chapter 15. Planning and SAT; Chapter 16. Software Verification; Chapter 17. Combinatorial Designs by SAT Solvers; Chapter 18. Connections to Statistical Physics; Chapter 19. MaxSAT; Chapter 20. Model Counting; Chapter 21. Non-Clausal SAT and ATPG; Chapter 22. Pseudo-Boolean and Cardinality Constraints; Chapter 23. QBF Theory; Chapter 24. QBFs reasoning; Chapter 25. SAT Techniques for Modal and Description Logics; Chapter 26. Satisfiability Modulo Theories; Chapter 27. Stochastic Boolean Satisfiability; Subject Index Cited Author IndexContributing Authors and Affiliations |
| Record Nr. | UNINA-9910778077003321 |
| Amsterdam, The Netherlands ; ; Washington, DC, : IOS Press, c2009 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Handbook of satisfiability / / edited by Armin Biere ... [et al.]
| Handbook of satisfiability / / edited by Armin Biere ... [et al.] |
| Edizione | [1st ed.] |
| Pubbl/distr/stampa | Amsterdam, The Netherlands ; ; Washington, DC, : IOS Press, c2009 |
| Descrizione fisica | 1 online resource (980 p.) |
| Disciplina | 006.3 |
| Altri autori (Persone) | BiereArmin |
| Collana | Frontiers in artificial intelligence and applications |
| Soggetto topico |
Propositional calculus
Decision making Computer algorithms Algebra, Boolean |
| ISBN |
1-4416-1678-0
1-60750-376-X 600-00-1439-2 |
| Classificazione |
ST 125
ST 300 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Title page; Contents; Part I. Theory and Algorithms; Chapter 1. A History of Satisfiability; Chapter 2. CNF Encodings; Chapter 3. Complete Algorithms; Chapter 4. CDCL Solvers; Chapter 5. Look-Ahead Based SAT Solvers; Chapter 6. Incomplete Algorithms; Chapter 7. Fundaments of Branching Heuristics; Chapter 8. Random Satisfiability; Chapter 9. Exploiting Runtime Variation in Complete Solvers; Chapter 10. Symmetry and Satisfiability; Chapter 11. Minimal Unsatisfiability and Autarkies; Chapter 12. Worst-Case Upper Bounds; Chapter 13. Fixed-Parameter Tractability
Part II. Applications and ExtensionsChapter 14. Bounded Model Checking; Chapter 15. Planning and SAT; Chapter 16. Software Verification; Chapter 17. Combinatorial Designs by SAT Solvers; Chapter 18. Connections to Statistical Physics; Chapter 19. MaxSAT; Chapter 20. Model Counting; Chapter 21. Non-Clausal SAT and ATPG; Chapter 22. Pseudo-Boolean and Cardinality Constraints; Chapter 23. QBF Theory; Chapter 24. QBFs reasoning; Chapter 25. SAT Techniques for Modal and Description Logics; Chapter 26. Satisfiability Modulo Theories; Chapter 27. Stochastic Boolean Satisfiability; Subject Index Cited Author IndexContributing Authors and Affiliations |
| Record Nr. | UNINA-9910822485403321 |
| Amsterdam, The Netherlands ; ; Washington, DC, : IOS Press, c2009 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Hardware and Software: Verification and Testing [[electronic resource] ] : 8th International Haifa Verification Conference, HVC 2012, Haifa, Israel, November 6-8, 2012. Revised Selected Papers / / edited by Armin Biere, Amir Nahir, Tanja Vos
| Hardware and Software: Verification and Testing [[electronic resource] ] : 8th International Haifa Verification Conference, HVC 2012, Haifa, Israel, November 6-8, 2012. Revised Selected Papers / / edited by Armin Biere, Amir Nahir, Tanja Vos |
| Edizione | [1st ed. 2013.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2013 |
| Descrizione fisica | 1 online resource (XII, 281 p. 75 illus.) |
| Disciplina | 005.14 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Software engineering
Programming languages (Electronic computers) Computer logic Artificial intelligence Mathematical logic Software Engineering Programming Languages, Compilers, Interpreters Logics and Meanings of Programs Artificial Intelligence Mathematical Logic and Formal Languages |
| ISBN | 3-642-39611-9 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | On Behavioral Programming -- Verifying Real-Time Software Is Not Reasonable: Abstract of Invited Talk -- SMT in Verification, Modeling, and Testing at Microsoft -- Reducing Costs While Increasing Quality -- Special Session on Security Verification -- Circuit Primitives for Monitoring Information Flow and Enabling Redundancy -- Formal Analysis of Security Data Paths in RTL Design -- Precise Detection of Atomicity Violations -- Proving Mutual Termination of Programs -- Knowledge Based Transactional Behavior -- Repair with On-The-Fly Program Analysis -- Computing Interpolants without Proofs -- MaxSAT-Based MCS Enumeration -- Automated Reencoding of Boolean Formulas. |
| Record Nr. | UNISA-996465985003316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2013 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Hardware and Software: Verification and Testing : 8th International Haifa Verification Conference, HVC 2012, Haifa, Israel, November 6-8, 2012. Revised Selected Papers / / edited by Armin Biere, Amir Nahir, Tanja Vos
| Hardware and Software: Verification and Testing : 8th International Haifa Verification Conference, HVC 2012, Haifa, Israel, November 6-8, 2012. Revised Selected Papers / / edited by Armin Biere, Amir Nahir, Tanja Vos |
| Edizione | [1st ed. 2013.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2013 |
| Descrizione fisica | 1 online resource (XII, 281 p. 75 illus.) |
| Disciplina | 005.14 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Software engineering
Programming languages (Electronic computers) Computer logic Artificial intelligence Mathematical logic Software Engineering Programming Languages, Compilers, Interpreters Logics and Meanings of Programs Artificial Intelligence Mathematical Logic and Formal Languages |
| ISBN | 3-642-39611-9 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | On Behavioral Programming -- Verifying Real-Time Software Is Not Reasonable: Abstract of Invited Talk -- SMT in Verification, Modeling, and Testing at Microsoft -- Reducing Costs While Increasing Quality -- Special Session on Security Verification -- Circuit Primitives for Monitoring Information Flow and Enabling Redundancy -- Formal Analysis of Security Data Paths in RTL Design -- Precise Detection of Atomicity Violations -- Proving Mutual Termination of Programs -- Knowledge Based Transactional Behavior -- Repair with On-The-Fly Program Analysis -- Computing Interpolants without Proofs -- MaxSAT-Based MCS Enumeration -- Automated Reencoding of Boolean Formulas. |
| Record Nr. | UNINA-9910483710003321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2013 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Theory and Applications of Satisfiability Testing - SAT 2006 [[electronic resource] ] : 9th International Conference, Seattle, WA, USA, August 12-15, 2006, Proceedings / / edited by Armin Biere, Carla P. Gomes
| Theory and Applications of Satisfiability Testing - SAT 2006 [[electronic resource] ] : 9th International Conference, Seattle, WA, USA, August 12-15, 2006, Proceedings / / edited by Armin Biere, Carla P. Gomes |
| Edizione | [1st ed. 2006.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2006 |
| Descrizione fisica | 1 online resource (XII, 440 p.) |
| Disciplina | 511.3 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Machine theory
Algorithms Operating systems (Computers) Numerical analysis Artificial intelligence Mathematical logic Formal Languages and Automata Theory Operating Systems Numerical Analysis Artificial Intelligence Mathematical Logic and Foundations |
| ISBN | 3-540-37207-5 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- From Propositional Satisfiability to Satisfiability Modulo Theories -- CSPs: Adding Structure to SAT -- Session 1. Proofs and Cores -- Complexity of Semialgebraic Proofs with Restricted Degree of Falsity -- Categorisation of Clauses in Conjunctive Normal Forms: Minimally Unsatisfiable Sub-clause-sets and the Lean Kernel -- A Scalable Algorithm for Minimal Unsatisfiable Core Extraction -- Minimum Witnesses for Unsatisfiable 2CNFs -- Preliminary Report on Input Cover Number as a Metric for Propositional Resolution Proofs -- Extended Resolution Proofs for Symbolic SAT Solving with Quantification -- Session 2. Heuristics and Algorithms -- Encoding CNFs to Empower Component Analysis -- Satisfiability Checking of Non-clausal Formulas Using General Matings -- Determinization of Resolution by an Algorithm Operating on Complete Assignments -- A Complete Random Jump Strategy with Guiding Paths -- Session 3. Applications -- Applications of SAT Solvers to Cryptanalysis of Hash Functions -- Functional Treewidth: Bounding Complexity in the Presence of Functional Dependencies -- Encoding the Satisfiability of Modal and Description Logics into SAT: The Case Study of K(m)/ -- SAT in Bioinformatics: Making the Case with Haplotype Inference -- Session 4. SMT -- Lemma Learning in SMT on Linear Constraints -- On SAT Modulo Theories and Optimization Problems -- Fast and Flexible Difference Constraint Propagation for DPLL(T) -- A Progressive Simplifier for Satisfiability Modulo Theories -- Session 5. Structure -- Dependency Quantified Horn Formulas: Models and Complexity -- On Linear CNF Formulas -- A Dichotomy Theorem for Typed Constraint Satisfaction Problems -- Session 6. MAX-SAT -- A Complete Calculus for Max-SAT -- On Solving the Partial MAX-SAT Problem -- MAX-SAT for Formulas with Constant Clause Density Can Be Solved Faster Than in Time -- Average-Case Analysis for the MAX-2SAT Problem -- Session 7. Local Search and Survey Propagation -- Local Search for Unsatisfiability -- Efficiency of Local Search -- Implementing Survey Propagation on Graphics Processing Units -- Characterizing Propagation Methods for Boolean Satisfiability -- Session 8. QBF -- Minimal False Quantified Boolean Formulas -- Binary Clause Reasoning in QBF -- Solving Quantified Boolean Formulas with Circuit Observability Don’t Cares -- QBF Modeling: Exploiting Player Symmetry for Simplicity and Efficiency -- Session 9. Counting and Concurrency -- Solving #SAT Using Vertex Covers -- Counting Models in Integer Domains -- sharpSAT – Counting Models with Advanced Component Caching and Implicit BCP -- A Distribution Method for Solving SAT in Grids. |
| Record Nr. | UNISA-996465581803316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2006 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Theory and applications of satisfiability testing--SAT 2006 : 9th international conference, Seattle, WA, USA, August 12-15, 2006 : proceedings / / Armin Biere, Carla P. Gomes (eds.)
| Theory and applications of satisfiability testing--SAT 2006 : 9th international conference, Seattle, WA, USA, August 12-15, 2006 : proceedings / / Armin Biere, Carla P. Gomes (eds.) |
| Edizione | [1st ed. 2006.] |
| Pubbl/distr/stampa | Berlin, : Springer, 2006 |
| Descrizione fisica | 1 online resource (XII, 440 p.) |
| Disciplina | 511.3 |
| Altri autori (Persone) |
BiereArmin
GomesCarla |
| Collana |
Lecture notes in computer science
LNCS sublibrary. SL 1, Theoretical computer science and general issues |
| Soggetto topico |
Propositional calculus
Decision making Computer algorithms Algebra, Boolean |
| ISBN | 3-540-37207-5 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- From Propositional Satisfiability to Satisfiability Modulo Theories -- CSPs: Adding Structure to SAT -- Session 1. Proofs and Cores -- Complexity of Semialgebraic Proofs with Restricted Degree of Falsity -- Categorisation of Clauses in Conjunctive Normal Forms: Minimally Unsatisfiable Sub-clause-sets and the Lean Kernel -- A Scalable Algorithm for Minimal Unsatisfiable Core Extraction -- Minimum Witnesses for Unsatisfiable 2CNFs -- Preliminary Report on Input Cover Number as a Metric for Propositional Resolution Proofs -- Extended Resolution Proofs for Symbolic SAT Solving with Quantification -- Session 2. Heuristics and Algorithms -- Encoding CNFs to Empower Component Analysis -- Satisfiability Checking of Non-clausal Formulas Using General Matings -- Determinization of Resolution by an Algorithm Operating on Complete Assignments -- A Complete Random Jump Strategy with Guiding Paths -- Session 3. Applications -- Applications of SAT Solvers to Cryptanalysis of Hash Functions -- Functional Treewidth: Bounding Complexity in the Presence of Functional Dependencies -- Encoding the Satisfiability of Modal and Description Logics into SAT: The Case Study of K(m)/ -- SAT in Bioinformatics: Making the Case with Haplotype Inference -- Session 4. SMT -- Lemma Learning in SMT on Linear Constraints -- On SAT Modulo Theories and Optimization Problems -- Fast and Flexible Difference Constraint Propagation for DPLL(T) -- A Progressive Simplifier for Satisfiability Modulo Theories -- Session 5. Structure -- Dependency Quantified Horn Formulas: Models and Complexity -- On Linear CNF Formulas -- A Dichotomy Theorem for Typed Constraint Satisfaction Problems -- Session 6. MAX-SAT -- A Complete Calculus for Max-SAT -- On Solving the Partial MAX-SAT Problem -- MAX-SAT for Formulas with Constant Clause Density Can Be Solved Faster Than in Time -- Average-Case Analysis for the MAX-2SAT Problem -- Session 7. Local Search and Survey Propagation -- Local Search for Unsatisfiability -- Efficiency of Local Search -- Implementing Survey Propagation on Graphics Processing Units -- Characterizing Propagation Methods for Boolean Satisfiability -- Session 8. QBF -- Minimal False Quantified Boolean Formulas -- Binary Clause Reasoning in QBF -- Solving Quantified Boolean Formulas with Circuit Observability Don’t Cares -- QBF Modeling: Exploiting Player Symmetry for Simplicity and Efficiency -- Session 9. Counting and Concurrency -- Solving #SAT Using Vertex Covers -- Counting Models in Integer Domains -- sharpSAT – Counting Models with Advanced Component Caching and Implicit BCP -- A Distribution Method for Solving SAT in Grids. |
| Altri titoli varianti | SAT 2006 |
| Record Nr. | UNINA-9910484504903321 |
| Berlin, : Springer, 2006 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Tools and Algorithms for the Construction and Analysis of Systems [[electronic resource] ] : 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25–30, 2020, Proceedings, Part II / / edited by Armin Biere, David Parker
| Tools and Algorithms for the Construction and Analysis of Systems [[electronic resource] ] : 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25–30, 2020, Proceedings, Part II / / edited by Armin Biere, David Parker |
| Autore | Biere Armin |
| Edizione | [1st ed. 2020.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2020 |
| Descrizione fisica | 1 online resource (XXIII, 425 p. 1 illus.) |
| Disciplina | 005.1 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Software engineering
Computers, Special purpose Computer systems Microprogramming Computer science—Mathematics Software Engineering Special Purpose and Application-Based Systems Computer System Implementation Control Structures and Microprogramming Mathematics of Computing |
| ISBN | 3-030-45237-9 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Bisimulation -- Verification and Efficiency -- Logic and Proof -- Tools and Case Studies -- Games and Automata -- SV-COMP 2020. |
| Record Nr. | UNISA-996418216303316 |
Biere Armin
|
||
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2020 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
