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.
Automated Reasoning [[electronic resource] ] : Second International Joint Conference, IJCAR 2004, Cork, Ireland, July 4-8, 2004, Proceedings / / edited by David Basin, Michael Rusinowitch
| Automated Reasoning [[electronic resource] ] : Second International Joint Conference, IJCAR 2004, Cork, Ireland, July 4-8, 2004, Proceedings / / edited by David Basin, Michael Rusinowitch |
| Edizione | [1st ed. 2004.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004 |
| Descrizione fisica | 1 online resource (XII, 491 p.) |
| Disciplina | 004.015113 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Artificial intelligence
Mathematical logic Computer logic Software engineering Artificial Intelligence Mathematical Logic and Foundations Mathematical Logic and Formal Languages Logics and Meanings of Programs Software Engineering |
| ISBN | 3-540-25984-8 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Rewriting -- Rewriting Logic Semantics: From Language Specifications to Formal Analysis Tools -- A Redundancy Criterion Based on Ground Reducibility by Ordered Rewriting -- Efficient Checking of Term Ordering Constraints -- Improved Modular Termination Proofs Using Dependency Pairs -- Deciding Fundamental Properties of Right-(Ground or Variable) Rewrite Systems by Rewrite Closure -- Saturation-Based Theorem Proving -- Redundancy Notions for Paramodulation with Non-monotonic Orderings -- A Resolution Decision Procedure for the Guarded Fragment with Transitive Guards -- Attacking a Protocol for Group Key Agreement by Refuting Incorrect Inductive Conjectures -- Combination Techniques -- Decision Procedures for Recursive Data Structures with Integer Constraints -- Modular Proof Systems for Partial Functions with Weak Equality -- A New Combination Procedure for the Word Problem That Generalizes Fusion Decidability Results in Modal Logics -- Verification and Systems -- Using Automated Theorem Provers to Certify Auto-generated Aerospace Software -- argo-lib: A Generic Platform for Decision Procedures -- The ICS Decision Procedures for Embedded Deduction -- System Description: E 0.81 -- Reasoning with Finite Structure -- Second-Order Logic over Finite Structures – Report on a Research Programme -- Efficient Algorithms for Constraint Description Problems over Finite Totally Ordered Domains -- Tableaux and Non-classical Logics -- PDL with Negation of Atomic Programs -- Counter-Model Search in Gödel-Dummett Logics -- Generalised Handling of Variables in Disconnection Tableaux -- Applications and Systems -- Chain Resolution for the Semantic Web -- Sonic — Non-standard Inferences Go OilEd -- TeMP: A Temporal Monodic Prover -- Dr.Doodle: A Diagrammatic Theorem Prover -- Computer Mathematics -- Solving Constraints by Elimination Methods -- Analyzing Selected Quantified Integer Programs -- Interactive Theorem Proving -- Formalizing O Notation in Isabelle/HOL -- Experiments on Supporting Interactive Proof Using Resolution -- A Machine-Checked Formalization of the Generic Model and the Random Oracle Model -- Combinatorial Reasoning -- Automatic Generation of Classification Theorems for Finite Algebras -- Efficient Algorithms for Computing Modulo Permutation Theories -- Overlapping Leaf Permutative Equations -- Higher-Order Reasoning -- TaMeD: A Tableau Method for Deduction Modulo -- Lambda Logic -- Formalizing Undefinedness Arising in Calculus -- Competition -- The CADE ATP System Competition. |
| Record Nr. | UNISA-996465722203316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Automated Reasoning : Second International Joint Conference, IJCAR 2004, Cork, Ireland, July 4-8, 2004, Proceedings / / edited by David Basin, Michael Rusinowitch
| Automated Reasoning : Second International Joint Conference, IJCAR 2004, Cork, Ireland, July 4-8, 2004, Proceedings / / edited by David Basin, Michael Rusinowitch |
| Edizione | [1st ed. 2004.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004 |
| Descrizione fisica | 1 online resource (XII, 491 p.) |
| Disciplina | 004.015113 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Artificial intelligence
Mathematical logic Computer logic Software engineering Artificial Intelligence Mathematical Logic and Foundations Mathematical Logic and Formal Languages Logics and Meanings of Programs Software Engineering |
| ISBN | 3-540-25984-8 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Rewriting -- Rewriting Logic Semantics: From Language Specifications to Formal Analysis Tools -- A Redundancy Criterion Based on Ground Reducibility by Ordered Rewriting -- Efficient Checking of Term Ordering Constraints -- Improved Modular Termination Proofs Using Dependency Pairs -- Deciding Fundamental Properties of Right-(Ground or Variable) Rewrite Systems by Rewrite Closure -- Saturation-Based Theorem Proving -- Redundancy Notions for Paramodulation with Non-monotonic Orderings -- A Resolution Decision Procedure for the Guarded Fragment with Transitive Guards -- Attacking a Protocol for Group Key Agreement by Refuting Incorrect Inductive Conjectures -- Combination Techniques -- Decision Procedures for Recursive Data Structures with Integer Constraints -- Modular Proof Systems for Partial Functions with Weak Equality -- A New Combination Procedure for the Word Problem That Generalizes Fusion Decidability Results in Modal Logics -- Verification and Systems -- Using Automated Theorem Provers to Certify Auto-generated Aerospace Software -- argo-lib: A Generic Platform for Decision Procedures -- The ICS Decision Procedures for Embedded Deduction -- System Description: E 0.81 -- Reasoning with Finite Structure -- Second-Order Logic over Finite Structures – Report on a Research Programme -- Efficient Algorithms for Constraint Description Problems over Finite Totally Ordered Domains -- Tableaux and Non-classical Logics -- PDL with Negation of Atomic Programs -- Counter-Model Search in Gödel-Dummett Logics -- Generalised Handling of Variables in Disconnection Tableaux -- Applications and Systems -- Chain Resolution for the Semantic Web -- Sonic — Non-standard Inferences Go OilEd -- TeMP: A Temporal Monodic Prover -- Dr.Doodle: A Diagrammatic Theorem Prover -- Computer Mathematics -- Solving Constraints by Elimination Methods -- Analyzing Selected Quantified Integer Programs -- Interactive Theorem Proving -- Formalizing O Notation in Isabelle/HOL -- Experiments on Supporting Interactive Proof Using Resolution -- A Machine-Checked Formalization of the Generic Model and the Random Oracle Model -- Combinatorial Reasoning -- Automatic Generation of Classification Theorems for Finite Algebras -- Efficient Algorithms for Computing Modulo Permutation Theories -- Overlapping Leaf Permutative Equations -- Higher-Order Reasoning -- TaMeD: A Tableau Method for Deduction Modulo -- Lambda Logic -- Formalizing Undefinedness Arising in Calculus -- Competition -- The CADE ATP System Competition. |
| Record Nr. | UNINA-9910144189203321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
FMSE '03 : proceedings of the 2003 ACM Workshop on Formal Methods in Security Engineering : Washington, DC, USA, October 30, 2003 : co-located with CCS'03
| FMSE '03 : proceedings of the 2003 ACM Workshop on Formal Methods in Security Engineering : Washington, DC, USA, October 30, 2003 : co-located with CCS'03 |
| Pubbl/distr/stampa | [Place of publication not identified], : ACM, 2003 |
| Descrizione fisica | 1 online resource (93 pages) |
| Collana | ACM Conferences |
| Soggetto topico |
Engineering & Applied Sciences
Computer Science |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Altri titoli varianti |
Formal Methods in Security Engineering '03 : proceedings of the 2003 Association for Computing Machinery Workshop on Formal Methods in Security Engineering : Washington, District of Columbia, United States of America, October 30, 2003 : co-located with Computer and Communications Security'03
Proceedings of the 2003 ACM Workshop on Formal Methods in Security Engineering |
| Record Nr. | UNINA-9910375934303321 |
| [Place of publication not identified], : ACM, 2003 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Principles of Security and Trust [[electronic resource] ] : Second International Conference, POST 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013, Proceedings / / edited by David Basin, John C. Mitchell
| Principles of Security and Trust [[electronic resource] ] : Second International Conference, POST 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013, Proceedings / / edited by David Basin, John C. Mitchell |
| Edizione | [1st ed. 2013.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2013 |
| Descrizione fisica | 1 online resource (XX, 287 p. 34 illus.) |
| Disciplina | 005.8 |
| Collana | Security and Cryptology |
| Soggetto topico |
Computer security
Computer communication systems Data encryption (Computer science) E-commerce Management information systems Computer science Systems and Data Security Computer Communication Networks Cryptology e-Commerce/e-business Management of Computing and Information Systems |
| ISBN | 3-642-36830-1 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Formal Analysis of Privacy for Routing Protocols in Mobile Ad Hoc Networks -- Practical Everlasting Privacy -- A Differentially Private Mechanism of Optimal Utility for a Region of Priors -- Proved Generation of Implementations from Computationally Secure Protocol Specifications -- Sound Security Protocol Transformations -- Logical Foundations of Secure Resource Management in Protocol Implementations -- Keys to the Cloud: Formal Analysis and Concrete Attacks on Encrypted Web Storage -- Lazy Mobile Intruders -- On Layout Randomization for Arrays and Functions -- A Theory of Agreements and Protection -- Computational Soundness of Symbolic Zero-Knowledge Proofs: Weaker Assumptions and Mechanized Verification -- Proving More Observational Equivalences with ProVerif -- Formal Verification of e-Auction Protocols -- Sessions and Separability in Security Protocols. |
| Record Nr. | UNISA-996465677703316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2013 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Principles of Security and Trust : Second International Conference, POST 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013, Proceedings / / edited by David Basin, John C. Mitchell
| Principles of Security and Trust : Second International Conference, POST 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013, Proceedings / / edited by David Basin, John C. Mitchell |
| Edizione | [1st ed. 2013.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2013 |
| Descrizione fisica | 1 online resource (XX, 287 p. 34 illus.) |
| Disciplina | 005.8 |
| Collana | Security and Cryptology |
| Soggetto topico |
Data protection
Computer networks Cryptography Data encryption (Computer science) Electronic commerce Electronic data processing—Management Data and Information Security Computer Communication Networks Cryptology e-Commerce and e-Business IT Operations |
| ISBN | 3-642-36830-1 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Formal Analysis of Privacy for Routing Protocols in Mobile Ad Hoc Networks -- Practical Everlasting Privacy -- A Differentially Private Mechanism of Optimal Utility for a Region of Priors -- Proved Generation of Implementations from Computationally Secure Protocol Specifications -- Sound Security Protocol Transformations -- Logical Foundations of Secure Resource Management in Protocol Implementations -- Keys to the Cloud: Formal Analysis and Concrete Attacks on Encrypted Web Storage -- Lazy Mobile Intruders -- On Layout Randomization for Arrays and Functions -- A Theory of Agreements and Protection -- Computational Soundness of Symbolic Zero-Knowledge Proofs: Weaker Assumptions and Mechanized Verification -- Proving More Observational Equivalences with ProVerif -- Formal Verification of e-Auction Protocols -- Sessions and Separability in Security Protocols. |
| Record Nr. | UNINA-9910739418303321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2013 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Proceedings of the Second Acm Conference on Wireless Network Security
| Proceedings of the Second Acm Conference on Wireless Network Security |
| Autore | Basin David |
| Pubbl/distr/stampa | [Place of publication not identified], : Association for Computing Machinery, 2009 |
| Descrizione fisica | 1 online resource (280 p.;) |
| Collana | ACM Conferences |
| Soggetto topico | Information Technology - Computer Science (Hardware & Networks) |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Altri titoli varianti | WiSec '09 |
| Record Nr. | UNINA-9910375802503321 |
Basin David
|
||
| [Place of publication not identified], : Association for Computing Machinery, 2009 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Theorem Proving in Higher Order Logics [[electronic resource] ] : 16th International Conference, TPHOLs 2003, Rom, Italy, September 8-12, 2003, Proceedings / / edited by David Basin, Burkhart Wolff
| Theorem Proving in Higher Order Logics [[electronic resource] ] : 16th International Conference, TPHOLs 2003, Rom, Italy, September 8-12, 2003, Proceedings / / edited by David Basin, Burkhart Wolff |
| Edizione | [1st ed. 2003.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2003 |
| Descrizione fisica | 1 online resource (X, 366 p.) |
| Disciplina | 006.333 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Philosophy
Mathematical logic Logic design Software engineering Computer logic Artificial intelligence Philosophy, general Mathematical Logic and Formal Languages Logic Design Software Engineering Logics and Meanings of Programs Artificial Intelligence |
| ISBN | 3-540-45130-7 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talk I -- Click’n Prove: Interactive Proofs within Set Theory -- Hardware and Assembler Languages -- Formal Specification and Verification of ARM6 -- A Programming Logic for Java Bytecode Programs -- Verified Bytecode Subroutines -- Proof Automation I -- Complete Integer Decision Procedures as Derived Rules in HOL -- Changing Data Representation within the Coq System -- Applications of Polytypism in Theorem Proving -- Proof Automation II -- A Coverage Checking Algorithm for LF -- Automatic Generation of Generalization Lemmas for Proving Properties of Tail-Recursive Definitions -- Tool Combination -- Embedding of Systems of Affine Recurrence Equations in Coq -- Programming a Symbolic Model Checker in a Fully Expansive Theorem Prover -- Combining Testing and Proving in Dependent Type Theory -- Invited Talk II -- Reasoning about Proof Search Specifications: An Abstract -- Logic Extensions -- Program Extraction from Large Proof Developments -- First Order Logic with Domain Conditions -- Extending Higher-Order Unification to Support Proof Irrelevance -- Advances in Theorem Prover Technology -- Inductive Invariants for Nested Recursion -- Implementing Modules in the Coq System -- MetaPRL – A Modular Logical Environment -- Mathematical Theories -- Proving Pearl: Knuth’s Algorithm for Prime Numbers -- Formalizing Hilbert’s Grundlagen in Isabelle/Isar -- Security -- Using Coq to Verify Java CardTM Applet Isolation Properties -- Verifying Second-Level Security Protocols. |
| Record Nr. | UNISA-996465962103316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2003 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Theorem Proving in Higher Order Logics : 16th International Conference, TPHOLs 2003, Rom, Italy, September 8-12, 2003, Proceedings / / edited by David Basin, Burkhart Wolff
| Theorem Proving in Higher Order Logics : 16th International Conference, TPHOLs 2003, Rom, Italy, September 8-12, 2003, Proceedings / / edited by David Basin, Burkhart Wolff |
| Edizione | [1st ed. 2003.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2003 |
| Descrizione fisica | 1 online resource (X, 366 p.) |
| Disciplina | 006.333 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Philosophy
Mathematical logic Logic design Software engineering Computer logic Artificial intelligence Philosophy, general Mathematical Logic and Formal Languages Logic Design Software Engineering Logics and Meanings of Programs Artificial Intelligence |
| ISBN | 3-540-45130-7 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talk I -- Click’n Prove: Interactive Proofs within Set Theory -- Hardware and Assembler Languages -- Formal Specification and Verification of ARM6 -- A Programming Logic for Java Bytecode Programs -- Verified Bytecode Subroutines -- Proof Automation I -- Complete Integer Decision Procedures as Derived Rules in HOL -- Changing Data Representation within the Coq System -- Applications of Polytypism in Theorem Proving -- Proof Automation II -- A Coverage Checking Algorithm for LF -- Automatic Generation of Generalization Lemmas for Proving Properties of Tail-Recursive Definitions -- Tool Combination -- Embedding of Systems of Affine Recurrence Equations in Coq -- Programming a Symbolic Model Checker in a Fully Expansive Theorem Prover -- Combining Testing and Proving in Dependent Type Theory -- Invited Talk II -- Reasoning about Proof Search Specifications: An Abstract -- Logic Extensions -- Program Extraction from Large Proof Developments -- First Order Logic with Domain Conditions -- Extending Higher-Order Unification to Support Proof Irrelevance -- Advances in Theorem Prover Technology -- Inductive Invariants for Nested Recursion -- Implementing Modules in the Coq System -- MetaPRL – A Modular Logical Environment -- Mathematical Theories -- Proving Pearl: Knuth’s Algorithm for Prime Numbers -- Formalizing Hilbert’s Grundlagen in Isabelle/Isar -- Security -- Using Coq to Verify Java CardTM Applet Isolation Properties -- Verifying Second-Level Security Protocols. |
| Record Nr. | UNINA-9910144027503321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2003 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||