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.
Interactive Theorem Proving [[electronic resource] ] : 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings / / edited by Jeremy Avigad, Assia Mahboubi
| Interactive Theorem Proving [[electronic resource] ] : 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings / / edited by Jeremy Avigad, Assia Mahboubi |
| Edizione | [1st ed. 2018.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2018 |
| Descrizione fisica | 1 online resource (XVII, 642 p. 103 illus.) |
| Disciplina | 004.015113 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Machine theory
Software engineering Artificial intelligence Computer science Compilers (Computer programs) Electronic digital computers—Evaluation Formal Languages and Automata Theory Software Engineering Artificial Intelligence Computer Science Logic and Foundations of Programming Compilers and Interpreters System Performance and Evaluation |
| ISBN | 3-319-94821-0 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNINA-9910349426503321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2018 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Interactive Theorem Proving [[electronic resource] ] : 8th International Conference, ITP 2017, Brasília, Brazil, September 26–29, 2017, Proceedings / / edited by Mauricio Ayala-Rincón, César A. Muñoz
| Interactive Theorem Proving [[electronic resource] ] : 8th International Conference, ITP 2017, Brasília, Brazil, September 26–29, 2017, Proceedings / / edited by Mauricio Ayala-Rincón, César A. Muñoz |
| Edizione | [1st ed. 2017.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2017 |
| Descrizione fisica | 1 online resource (XIX, 532 p. 79 illus.) |
| Disciplina | 511.36028563 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Machine theory
Computer science Electronic digital computers—Evaluation Software engineering Compilers (Computer programs) Artificial intelligence Formal Languages and Automata Theory Computer Science Logic and Foundations of Programming System Performance and Evaluation Software Engineering Compilers and Interpreters Artificial Intelligence |
| ISBN | 3-319-66107-8 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Whitebox Automation -- Automated Theory Exploration for Interactive Theorem Proving: An Introduction to the Hipster System -- Automating Formalization by Statistical and Semantic Parsing of Mathematics -- A Formalization of Convex Polyhedra Based on the Simplex Method -- A Formal Proof of the Expressiveness of Deep Learning -- Formalization of the Lindemann-Weierstrass Theorem -- CompCertS: A Memory-Aware Verified C Compiler Using Pointer as Integer Semantics -- Formal Verification of a Floating-Point Expansion Renormalization Algorithm -- How to Simulate It in Isabelle: Towards Formal Proof for Secure Multi-Party Computation -- FoCaLiZe and Dedukti to the Rescue for Proof Interoperability -- A Formal Proof in Coq of LaSalle's Invariance Principle -- How to Get More out of Your Oracles -- Certifying Standard and Stratified Datalog Inference Engines in SSReect -- Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq -- Bellerophon: Tactical Theorem Proving for Hybrid Systems -- Formalizing Basic Quaternionic Analysis -- A Formalized General Theory of Syntax with Bindings -- Proof Certificates in PVS -- Efficient, Verified Checking of Propositional Proofs -- Proof Tactics for Assertions in Separation Logic -- Categoricity Results for Second-Order ZF in Dependent Type Theory -- Making PVS Accessible to Generic Services by Interpretation in a Universal Format -- Formally Verified Safe Vertical Maneuvers for Non-Deterministic, Accelerating Aircraft Dynamics -- Using Abstract Stobjs in ACL2 to Compute Matrix Normal Forms -- Typing Total Recursive Functions in Coq -- Effect Polymorphism in Higher-Order Logic (Proof Pearl) -- Schulze Voting as Evidence Carrying Computation -- Verified Spilling and Translation Validation with Repair -- A Verified Generational Garbage Collector for CakeML -- A Formalisation of Consistent Consequence for Boolean Equation Systems -- Homotopy Type Theory in Lean -- Verifying a Concurrent Garbage Collector Using a Rely-Guarantee Methodology -- Formalization of the Fundamental Group in Untyped Set Theory Using auto2. |
| Record Nr. | UNINA-9910484560503321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2017 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Interactive Theorem Proving [[electronic resource] ] : 8th International Conference, ITP 2017, Brasília, Brazil, September 26–29, 2017, Proceedings / / edited by Mauricio Ayala-Rincón, César A. Muñoz
| Interactive Theorem Proving [[electronic resource] ] : 8th International Conference, ITP 2017, Brasília, Brazil, September 26–29, 2017, Proceedings / / edited by Mauricio Ayala-Rincón, César A. Muñoz |
| Edizione | [1st ed. 2017.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2017 |
| Descrizione fisica | 1 online resource (XIX, 532 p. 79 illus.) |
| Disciplina | 511.36028563 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Machine theory
Computer science Electronic digital computers—Evaluation Software engineering Compilers (Computer programs) Artificial intelligence Formal Languages and Automata Theory Computer Science Logic and Foundations of Programming System Performance and Evaluation Software Engineering Compilers and Interpreters Artificial Intelligence |
| ISBN | 3-319-66107-8 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Whitebox Automation -- Automated Theory Exploration for Interactive Theorem Proving: An Introduction to the Hipster System -- Automating Formalization by Statistical and Semantic Parsing of Mathematics -- A Formalization of Convex Polyhedra Based on the Simplex Method -- A Formal Proof of the Expressiveness of Deep Learning -- Formalization of the Lindemann-Weierstrass Theorem -- CompCertS: A Memory-Aware Verified C Compiler Using Pointer as Integer Semantics -- Formal Verification of a Floating-Point Expansion Renormalization Algorithm -- How to Simulate It in Isabelle: Towards Formal Proof for Secure Multi-Party Computation -- FoCaLiZe and Dedukti to the Rescue for Proof Interoperability -- A Formal Proof in Coq of LaSalle's Invariance Principle -- How to Get More out of Your Oracles -- Certifying Standard and Stratified Datalog Inference Engines in SSReect -- Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq -- Bellerophon: Tactical Theorem Proving for Hybrid Systems -- Formalizing Basic Quaternionic Analysis -- A Formalized General Theory of Syntax with Bindings -- Proof Certificates in PVS -- Efficient, Verified Checking of Propositional Proofs -- Proof Tactics for Assertions in Separation Logic -- Categoricity Results for Second-Order ZF in Dependent Type Theory -- Making PVS Accessible to Generic Services by Interpretation in a Universal Format -- Formally Verified Safe Vertical Maneuvers for Non-Deterministic, Accelerating Aircraft Dynamics -- Using Abstract Stobjs in ACL2 to Compute Matrix Normal Forms -- Typing Total Recursive Functions in Coq -- Effect Polymorphism in Higher-Order Logic (Proof Pearl) -- Schulze Voting as Evidence Carrying Computation -- Verified Spilling and Translation Validation with Repair -- A Verified Generational Garbage Collector for CakeML -- A Formalisation of Consistent Consequence for Boolean Equation Systems -- Homotopy Type Theory in Lean -- Verifying a Concurrent Garbage Collector Using a Rely-Guarantee Methodology -- Formalization of the Fundamental Group in Untyped Set Theory Using auto2. |
| Record Nr. | UNISA-996465571103316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2017 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Interactive Theorem Proving [[electronic resource] ] : 7th International Conference, ITP 2016, Nancy, France, August 22-25, 2016, Proceedings / / edited by Jasmin Christian Blanchette, Stephan Merz
| Interactive Theorem Proving [[electronic resource] ] : 7th International Conference, ITP 2016, Nancy, France, August 22-25, 2016, Proceedings / / edited by Jasmin Christian Blanchette, Stephan Merz |
| Edizione | [1st ed. 2016.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2016 |
| Descrizione fisica | 1 online resource (XVII, 502 p. 88 illus.) |
| Disciplina | 004.015113 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Machine theory
Computer science Algorithms Software engineering Electronic digital computers—Evaluation Computer simulation Formal Languages and Automata Theory Computer Science Logic and Foundations of Programming Software Engineering System Performance and Evaluation Computer Modelling |
| ISBN | 3-319-43144-7 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNISA-996466035703316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2016 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Interactive Theorem Proving [[electronic resource] ] : 7th International Conference, ITP 2016, Nancy, France, August 22-25, 2016, Proceedings / / edited by Jasmin Christian Blanchette, Stephan Merz
| Interactive Theorem Proving [[electronic resource] ] : 7th International Conference, ITP 2016, Nancy, France, August 22-25, 2016, Proceedings / / edited by Jasmin Christian Blanchette, Stephan Merz |
| Edizione | [1st ed. 2016.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2016 |
| Descrizione fisica | 1 online resource (XVII, 502 p. 88 illus.) |
| Disciplina | 004.015113 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Machine theory
Computer science Algorithms Software engineering Electronic digital computers—Evaluation Computer simulation Formal Languages and Automata Theory Computer Science Logic and Foundations of Programming Software Engineering System Performance and Evaluation Computer Modelling |
| ISBN | 3-319-43144-7 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNINA-9910483136503321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2016 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Model Checking Software [[electronic resource] ] : 26th International Symposium, SPIN 2019, Beijing, China, July 15–16, 2019, Proceedings / / edited by Fabrizio Biondi, Thomas Given-Wilson, Axel Legay
| Model Checking Software [[electronic resource] ] : 26th International Symposium, SPIN 2019, Beijing, China, July 15–16, 2019, Proceedings / / edited by Fabrizio Biondi, Thomas Given-Wilson, Axel Legay |
| Edizione | [1st ed. 2019.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 |
| Descrizione fisica | 1 online resource (X, 261 p. 605 illus., 41 illus. in color.) |
| Disciplina | 005.14 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Software engineering
Computer science Algorithms Machine theory Computer simulation Electronic digital computers—Evaluation Software Engineering Computer Science Logic and Foundations of Programming Formal Languages and Automata Theory Computer Modelling System Performance and Evaluation |
| ISBN | 3-030-30923-1 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Model Verification Through Dependency Graphs -- Model Checking Branching Time Properties for Incomplete Markov Chains -- A Novel Decentralized LTL Monitoring Framework Using Formula Progression Table -- From Dynamic State Machines to Promela -- String abstraction for model checking of C programs -- Swarm Model Checking on the GPU -- Statistical Model Checking of Complex Robotic Systems -- STAD: Stack Trace Based Automatic Software Misconfiguration Diagnosis via Value Dependency Graph -- Extracting Safe Thread Schedules from Incomplete Model Checking Results -- Learning Guided Enumerative Synthesis for Superoptimization -- Applying Model Checking Approach with Floating Point Arithmetic -- Conformance Testing of Schedulers for DSL-based Model Checking -- A Study of Learning Data Structure Invariants Using Off-the-shelf Tools -- VeriVANca: An Actor-Based Framework for Formal Verification of Warning Message Dissemination Schemes in VANETs. |
| Record Nr. | UNISA-996466423203316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Model Checking Software [[electronic resource] ] : 26th International Symposium, SPIN 2019, Beijing, China, July 15–16, 2019, Proceedings / / edited by Fabrizio Biondi, Thomas Given-Wilson, Axel Legay
| Model Checking Software [[electronic resource] ] : 26th International Symposium, SPIN 2019, Beijing, China, July 15–16, 2019, Proceedings / / edited by Fabrizio Biondi, Thomas Given-Wilson, Axel Legay |
| Edizione | [1st ed. 2019.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 |
| Descrizione fisica | 1 online resource (X, 261 p. 605 illus., 41 illus. in color.) |
| Disciplina | 005.14 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Software engineering
Computer science Algorithms Machine theory Computer simulation Electronic digital computers—Evaluation Software Engineering Computer Science Logic and Foundations of Programming Formal Languages and Automata Theory Computer Modelling System Performance and Evaluation |
| ISBN | 3-030-30923-1 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Model Verification Through Dependency Graphs -- Model Checking Branching Time Properties for Incomplete Markov Chains -- A Novel Decentralized LTL Monitoring Framework Using Formula Progression Table -- From Dynamic State Machines to Promela -- String abstraction for model checking of C programs -- Swarm Model Checking on the GPU -- Statistical Model Checking of Complex Robotic Systems -- STAD: Stack Trace Based Automatic Software Misconfiguration Diagnosis via Value Dependency Graph -- Extracting Safe Thread Schedules from Incomplete Model Checking Results -- Learning Guided Enumerative Synthesis for Superoptimization -- Applying Model Checking Approach with Floating Point Arithmetic -- Conformance Testing of Schedulers for DSL-based Model Checking -- A Study of Learning Data Structure Invariants Using Off-the-shelf Tools -- VeriVANca: An Actor-Based Framework for Formal Verification of Warning Message Dissemination Schemes in VANETs. |
| Record Nr. | UNINA-9910349277503321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Parallel and Distributed Processing and Applications [[electronic resource] ] : 5th International Symposium, ISPA 2007, Niagara Falls, Canada, August 29-31, 2007, Proceedings / / edited by Ivan Stojmenovic, Ruppa K. Thulasiram, Laurence T. Yang, Weijia Jia, Minyi Guo, Rodrigo Fernandes de Mello
| Parallel and Distributed Processing and Applications [[electronic resource] ] : 5th International Symposium, ISPA 2007, Niagara Falls, Canada, August 29-31, 2007, Proceedings / / edited by Ivan Stojmenovic, Ruppa K. Thulasiram, Laurence T. Yang, Weijia Jia, Minyi Guo, Rodrigo Fernandes de Mello |
| Edizione | [1st ed. 2007.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 |
| Descrizione fisica | 1 online resource (XX, 1000 p.) |
| Disciplina | 004.35 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer systems
Algorithms Computer networks Application software Electronic digital computers—Evaluation Software engineering Computer System Implementation Computer Communication Networks Computer and Information Systems Applications System Performance and Evaluation Software Engineering |
| ISBN | 3-540-74742-7 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Keynote Speech -- Algorithms and Applications -- Architectures and Systems -- Datamining and Databases -- Fault Tolerance and Security -- Middleware and Cooperative Computing -- Networks -- Software and Languages. |
| Record Nr. | UNISA-996465338303316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Parallel and Distributed Processing and Applications [[electronic resource] ] : 5th International Symposium, ISPA 2007, Niagara Falls, Canada, August 29-31, 2007, Proceedings / / edited by Ivan Stojmenovic, Ruppa K. Thulasiram, Laurence T. Yang, Weijia Jia, Minyi Guo, Rodrigo Fernandes de Mello
| Parallel and Distributed Processing and Applications [[electronic resource] ] : 5th International Symposium, ISPA 2007, Niagara Falls, Canada, August 29-31, 2007, Proceedings / / edited by Ivan Stojmenovic, Ruppa K. Thulasiram, Laurence T. Yang, Weijia Jia, Minyi Guo, Rodrigo Fernandes de Mello |
| Edizione | [1st ed. 2007.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 |
| Descrizione fisica | 1 online resource (XX, 1000 p.) |
| Disciplina | 004.35 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer systems
Algorithms Computer networks Application software Electronic digital computers—Evaluation Software engineering Computer System Implementation Computer Communication Networks Computer and Information Systems Applications System Performance and Evaluation Software Engineering |
| ISBN | 3-540-74742-7 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Keynote Speech -- Algorithms and Applications -- Architectures and Systems -- Datamining and Databases -- Fault Tolerance and Security -- Middleware and Cooperative Computing -- Networks -- Software and Languages. |
| Record Nr. | UNINA-9910484632903321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Parallel and Distributed Processing and Applications [[electronic resource] ] : 4th International Symposium, ISPA 2006, Sorrento, Italy, December 4-6, 2006, Proceedings / / edited by Minyi Guo, Laurence T. Yang, Beniamino Di Martino, Hans Zima, Jack Dongarra, Feilong Tang
| Parallel and Distributed Processing and Applications [[electronic resource] ] : 4th International Symposium, ISPA 2006, Sorrento, Italy, December 4-6, 2006, Proceedings / / edited by Minyi Guo, Laurence T. Yang, Beniamino Di Martino, Hans Zima, Jack Dongarra, Feilong Tang |
| Edizione | [1st ed. 2006.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2006 |
| Descrizione fisica | 1 online resource (XVIII, 953 p.) |
| Disciplina | 004.35 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer systems
Algorithms Computer networks Application software Electronic digital computers—Evaluation Software engineering Computer System Implementation Computer Communication Networks Computer and Information Systems Applications System Performance and Evaluation Software Engineering |
| ISBN | 3-540-68070-5 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Keynote Speech -- Track 1. Architectures and Networks -- Track 2. Languages and Algorithms -- Track 3. Middleware and Cooperative Computing -- Track 4. Software and Applications. |
| Record Nr. | UNISA-996466008203316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2006 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
