Design and Implementation of Symbolic Computation Systems [[electronic resource] ] : International Symposium DISCO '90, Capri, Italy, April 10-12, 1990. Proceedings / / edited by Alfonso Miola |
Edizione | [1st ed. 1990.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1990 |
Descrizione fisica | 1 online resource (XII, 286 p.) |
Disciplina | 004.2/1 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Computers
Computer programming Software engineering Programming languages (Electronic computers) Artificial intelligence Computer graphics Theory of Computation Programming Techniques Software Engineering Programming Languages, Compilers, Interpreters Artificial Intelligence Computer Graphics |
ISBN | 3-540-47014-X |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Current problems in computer algebra systems design -- The design of cayley — a language for modern algebra -- CoCoA: A user-friendly system for commutative algebra -- The design of SISYPHE : a system for doing symbolic and algebraic computations -- Scratchpad's view of algebra I: Basic commutative algebra -- Design issues for a computed-aided environment for constructive mathematics -- Efficient type inference and coercion in computer algebra -- Abstract specification of mathematical structures and methods -- Programming paradigms for symbolic computation systems analysis of an example -- The computation of Gröbner bases on a shared memory multiprocessor -- A theory for program and data type specification -- Context induction: A proof principle for behavioural abstractions -- Completion modulo associativity, commutativity and identity (AC1) -- Polymorphic type checking with subtypes in Prolog -- On the power of subsumption and context checks -- Putting algebraic components together: A dependent type approach -- The use of proof plans in formal methods -- A prolog technology theorem prover: A new exposition and implementation in Prolog -- Parametric queries, linear constraints and variable elimination -- AC-unification race: The system solving approach and its implementation -- Heuristical criteria in refutational theorem proving -- Requirements for standards in knowledge base systems -- Reconciling symbolic and numeric computation in a practical setting -- The design and specification of the ASSPEGIQUE database -- A functional and logic language with polymorphic types -- Graphical object oriented executable specification for an automation oriented paradigm of software development -- Building graphic user interfaces for computer algebra systems -- A system independent graphing package for mathematical functions -- A model of interaction for graphical systems -- Praxis: A rule-based expert system for MACSYMA -- Will DELiA grow into an expert system? -- The GANITH algebraic geometry toolkit -- Mas Modula-2 algebra system -- Prototypes for the automatic translation of computer algebra languages -- The implementation of A PC-based list processor for symbolic computation -- Implementation of the symbol analytic transformations language FLAC -- Design and development of ENprover, an automated theorem proving system based on EN-strategy -- Towards a logic language: An object-oriented implementation of the connection method -- Suggestions for a friendlier user interface. |
Record Nr. | UNISA-996465624703316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1990 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|
Tools and Algorithms for the Construction and Analysis of Systems [[electronic resource] ] : 8th International Conference, TACAS 2002, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002, Grenoble, France, April 8-12, 2002. Proceedings / / edited by Joost-Pieter Katoen, Perdita Stevens |
Edizione | [1st ed. 2002.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2002 |
Descrizione fisica | 1 online resource (XIV, 486 p.) |
Disciplina | 004.2/1 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Computers
Computer logic Software engineering Computer communication systems Algorithms Theory of Computation Logics and Meanings of Programs Software Engineering Computer Communication Networks Algorithm Analysis and Problem Complexity |
ISBN | 3-540-46002-0 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Invited Contributions -- Software Construction and Analysis Tools for Future Space Missions -- Alloy: A New Technology for Software Modelling -- Real-Time and Probabilistic Systems -- Improving the Verification of Timed Systems Using Influence Information -- Digitisation and Full Abstraction for Dense-Time Model Checking -- Probabilistic Symbolic Model Checking with PRISM: A Hybrid Approach -- Scheduling -- Timed Automata with Asynchronous Processes: Schedulability and Decidability -- Validating Timing Constraints of Dependent Jobs with Variable Execution Times in Distributed Real-Time Systems -- An Analysis of Zero-Clairvoyant Scheduling -- Preemptive Job-Shop Scheduling Using Stopwatch Automata -- Miscellaneous -- Explicit Modeling of Influences, and of Their Absence, in Distributed Systems -- A Functional Semantics of Attribute Grammars -- Software Verification -- Relative Completeness of Abstraction Refinement for Software Model Checking -- Towards the Automated Verification of Multithreaded Java Programs -- CLPS-B—A Constraint Solver for B -- Formal Verification of Functional Properties of an SCR-Style Software Requirements Specification Using PVS -- Infinite-State and Parametric Systems -- Beyond Parameterized Verification -- Resource-Constrained Model Checking of Recursive Programs -- Model Checking Large-Scale and Parameterized Resource Allocation Systems -- Model Checking: Logics and Algorithms -- Exploring Very Large State Spaces Using Genetic Algorithms -- Local Model-Checking of Modal Mu-Calculus on Acyclic Labeled Transition Systems -- The ForSpec Temporal Logic: A New Temporal Property-Specification Language -- Fine-Grain Conjunction Scheduling for Symbolic Reachability Analysis -- Model Checking and Testing -- A Temporal Logic Based Theory of Test Coverage and Generation -- Synthesizing Monitors for Safety Properties -- Adaptive Model Checking -- Partial-Order and Simulation Techniques -- Parallelisation of the Petri Net Unfolding Algorithm -- Black Box Unfolding with Local First Search -- Applicability of Fair Simulation -- Simulation as Coarsest Partition Problem -- Debugging with Model Checking -- Temporal Debugging for Concurrent Systems -- Fate and FreeWill in Error Traces -- Tool Papers -- TIMES b— A Tool for Modelling and Implementation of Embedded Systems -- Compositional Verification Using SVL Scripts -- STG: A Symbolic Test Generation Tool -- Real-Time Systems Design with PEP. |
Record Nr. | UNINA-9910143914703321 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2002 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|
Tools and Algorithms for the Construction and Analysis of Systems [[electronic resource] ] : 8th International Conference, TACAS 2002, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002, Grenoble, France, April 8-12, 2002. Proceedings / / edited by Joost-Pieter Katoen, Perdita Stevens |
Edizione | [1st ed. 2002.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2002 |
Descrizione fisica | 1 online resource (XIV, 486 p.) |
Disciplina | 004.2/1 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Computers
Computer logic Software engineering Computer communication systems Algorithms Theory of Computation Logics and Meanings of Programs Software Engineering Computer Communication Networks Algorithm Analysis and Problem Complexity |
ISBN | 3-540-46002-0 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Invited Contributions -- Software Construction and Analysis Tools for Future Space Missions -- Alloy: A New Technology for Software Modelling -- Real-Time and Probabilistic Systems -- Improving the Verification of Timed Systems Using Influence Information -- Digitisation and Full Abstraction for Dense-Time Model Checking -- Probabilistic Symbolic Model Checking with PRISM: A Hybrid Approach -- Scheduling -- Timed Automata with Asynchronous Processes: Schedulability and Decidability -- Validating Timing Constraints of Dependent Jobs with Variable Execution Times in Distributed Real-Time Systems -- An Analysis of Zero-Clairvoyant Scheduling -- Preemptive Job-Shop Scheduling Using Stopwatch Automata -- Miscellaneous -- Explicit Modeling of Influences, and of Their Absence, in Distributed Systems -- A Functional Semantics of Attribute Grammars -- Software Verification -- Relative Completeness of Abstraction Refinement for Software Model Checking -- Towards the Automated Verification of Multithreaded Java Programs -- CLPS-B—A Constraint Solver for B -- Formal Verification of Functional Properties of an SCR-Style Software Requirements Specification Using PVS -- Infinite-State and Parametric Systems -- Beyond Parameterized Verification -- Resource-Constrained Model Checking of Recursive Programs -- Model Checking Large-Scale and Parameterized Resource Allocation Systems -- Model Checking: Logics and Algorithms -- Exploring Very Large State Spaces Using Genetic Algorithms -- Local Model-Checking of Modal Mu-Calculus on Acyclic Labeled Transition Systems -- The ForSpec Temporal Logic: A New Temporal Property-Specification Language -- Fine-Grain Conjunction Scheduling for Symbolic Reachability Analysis -- Model Checking and Testing -- A Temporal Logic Based Theory of Test Coverage and Generation -- Synthesizing Monitors for Safety Properties -- Adaptive Model Checking -- Partial-Order and Simulation Techniques -- Parallelisation of the Petri Net Unfolding Algorithm -- Black Box Unfolding with Local First Search -- Applicability of Fair Simulation -- Simulation as Coarsest Partition Problem -- Debugging with Model Checking -- Temporal Debugging for Concurrent Systems -- Fate and FreeWill in Error Traces -- Tool Papers -- TIMES b— A Tool for Modelling and Implementation of Embedded Systems -- Compositional Verification Using SVL Scripts -- STG: A Symbolic Test Generation Tool -- Real-Time Systems Design with PEP. |
Record Nr. | UNISA-996465391203316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2002 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|
Tools and Algorithms for the Construction and Analysis of Systems [[electronic resource] ] : 4th International Conference, TACAS'98, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS'98, Lisbon, Portugal, March 28 - April 4, 1998, Proceedings / / edited by Bernhard Steffen |
Edizione | [1st ed. 1998.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1998 |
Descrizione fisica | 1 online resource (XV, 461 p.) |
Disciplina | 004.2/1 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Computers
Computer logic Software engineering Computer communication systems Theory of Computation Logics and Meanings of Programs Software Engineering Computer Communication Networks |
ISBN | 3-540-69753-5 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Formal verification of pipelined processors -- Fully local and efficient evaluation of alternating fixed points -- Modular model checking of software -- Verification based on local states -- Exploiting symmetry in linear time temporal logic model checking: One step beyond -- OPEN/CÆSAR: An open software architecture for verification, simulation, and testing -- Practical model-checking using games -- Combining finite automata, parallel programs and SDL using Petri nets -- Mesa: Support for scenario-based design of concurrent systems -- Efficient modeling of memory arrays in symbolic ternary simulation -- Translation validation -- A verified model checker for the modal ?-calculus in Coq -- Detecting races in relay ladder logic programs -- Verification of large state/event systems using compositionality and dependency analysis -- Tamagotchis need not die — Verification of statemate designs -- Modeling and verification of sC++ applications -- Factotum: Automatic and systematic sharing support for systems analyzers -- Model checking via reachability testing for timed automata -- Formal design and analysis of a gear controller -- Verifying networks of timed processes -- Model checking of real-time reachability properties using abstractions -- Symbolic exploration of transition hierarchies -- Static partial order reduction -- Set-based analysis of reactive infinite-state systems -- Deciding fixed and non-fixed size bit-vectors -- Experience with literate programming in the modelling and validation of systems -- A proof of burns N-process mutual exclusion algorithm using abstraction -- Automated verification of Szymanski's algorithm -- Formal verification of SDL systems at the siemens mobile phone department. |
Record Nr. | UNINA-9910143454103321 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1998 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|
Tools and Algorithms for the Construction and Analysis of Systems [[electronic resource] ] : 4th International Conference, TACAS'98, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS'98, Lisbon, Portugal, March 28 - April 4, 1998, Proceedings / / edited by Bernhard Steffen |
Edizione | [1st ed. 1998.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1998 |
Descrizione fisica | 1 online resource (XV, 461 p.) |
Disciplina | 004.2/1 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Computers
Computer logic Software engineering Computer communication systems Theory of Computation Logics and Meanings of Programs Software Engineering Computer Communication Networks |
ISBN | 3-540-69753-5 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Formal verification of pipelined processors -- Fully local and efficient evaluation of alternating fixed points -- Modular model checking of software -- Verification based on local states -- Exploiting symmetry in linear time temporal logic model checking: One step beyond -- OPEN/CÆSAR: An open software architecture for verification, simulation, and testing -- Practical model-checking using games -- Combining finite automata, parallel programs and SDL using Petri nets -- Mesa: Support for scenario-based design of concurrent systems -- Efficient modeling of memory arrays in symbolic ternary simulation -- Translation validation -- A verified model checker for the modal ?-calculus in Coq -- Detecting races in relay ladder logic programs -- Verification of large state/event systems using compositionality and dependency analysis -- Tamagotchis need not die — Verification of statemate designs -- Modeling and verification of sC++ applications -- Factotum: Automatic and systematic sharing support for systems analyzers -- Model checking via reachability testing for timed automata -- Formal design and analysis of a gear controller -- Verifying networks of timed processes -- Model checking of real-time reachability properties using abstractions -- Symbolic exploration of transition hierarchies -- Static partial order reduction -- Set-based analysis of reactive infinite-state systems -- Deciding fixed and non-fixed size bit-vectors -- Experience with literate programming in the modelling and validation of systems -- A proof of burns N-process mutual exclusion algorithm using abstraction -- Automated verification of Szymanski's algorithm -- Formal verification of SDL systems at the siemens mobile phone department. |
Record Nr. | UNISA-996466105003316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1998 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|
Tools and Algorithms for the Construction and Analysis of Systems [[electronic resource] ] : Third International Workshop, TACAS'97, Enschede, The Netherlands, April 2-4, 1997, Proceedings / / edited by Ed Brinksma |
Edizione | [1st ed. 1997.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1997 |
Descrizione fisica | 1 online resource (X, 437 p.) |
Disciplina | 004.2/1 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Computer engineering
Computers Software engineering Computer logic Computer communication systems Computer Engineering Theory of Computation Software Engineering Logics and Meanings of Programs Computer Communication Networks |
ISBN | 3-540-68519-7 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Hardware and software synthesis, optimization, and verification from Esterel programs -- Manipulation algorithms for K*BMDs -- Combining partial order and symmetry reductions -- Partial model checking with ROBDDs -- Space efficient reachability analysis through use of pseudo-root states -- The reference component of PEP -- A tool to support formal reasoning about computer languages -- The term processor generator Kimwitu -- Graphs in MetaFrame: The unifying power of polymorphism -- A tableau system for linear-TIME temporal logic -- Model-checking for a subclass of event structures -- Real-time logics: Fictitious clock as an abstraction of dense time -- Mosel: A flexible toolset for monadic second-order logic -- A brief introduction to coloured Petri Nets -- Design/CPN — A computer tool for Coloured Petri Nets -- Formal verification of statecharts with instantaneous chain reactions -- Compositional state space generation from Lotos programs -- Syntactic detection of process divergence and non-local choice in message sequence charts -- An automata based verification environment for mobile processes -- Compositional performance analysis -- Incremental development of deadlock-free communicating systems -- Automatic synthesis of specifications from the dynamic observation of reactive programs -- Visual verification of reactive systems -- Theorem prover support for the refinement of stream processing functions -- Integration in PVS: Tables, types, and model checking -- Test generation for intelligent networks using model checking -- Mechanically verified self-stabilizing hierarchical algorithms -- The bounded retransmission protocol must be on time!. |
Record Nr. | UNISA-996465533403316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1997 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|
Tools and Algorithms for the Construction and Analysis of Systems [[electronic resource] ] : Third International Workshop, TACAS'97, Enschede, The Netherlands, April 2-4, 1997, Proceedings / / edited by Ed Brinksma |
Edizione | [1st ed. 1997.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1997 |
Descrizione fisica | 1 online resource (X, 437 p.) |
Disciplina | 004.2/1 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Computer engineering
Computers Software engineering Computer logic Computer communication systems Computer Engineering Theory of Computation Software Engineering Logics and Meanings of Programs Computer Communication Networks |
ISBN | 3-540-68519-7 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Hardware and software synthesis, optimization, and verification from Esterel programs -- Manipulation algorithms for K*BMDs -- Combining partial order and symmetry reductions -- Partial model checking with ROBDDs -- Space efficient reachability analysis through use of pseudo-root states -- The reference component of PEP -- A tool to support formal reasoning about computer languages -- The term processor generator Kimwitu -- Graphs in MetaFrame: The unifying power of polymorphism -- A tableau system for linear-TIME temporal logic -- Model-checking for a subclass of event structures -- Real-time logics: Fictitious clock as an abstraction of dense time -- Mosel: A flexible toolset for monadic second-order logic -- A brief introduction to coloured Petri Nets -- Design/CPN — A computer tool for Coloured Petri Nets -- Formal verification of statecharts with instantaneous chain reactions -- Compositional state space generation from Lotos programs -- Syntactic detection of process divergence and non-local choice in message sequence charts -- An automata based verification environment for mobile processes -- Compositional performance analysis -- Incremental development of deadlock-free communicating systems -- Automatic synthesis of specifications from the dynamic observation of reactive programs -- Visual verification of reactive systems -- Theorem prover support for the refinement of stream processing functions -- Integration in PVS: Tables, types, and model checking -- Test generation for intelligent networks using model checking -- Mechanically verified self-stabilizing hierarchical algorithms -- The bounded retransmission protocol must be on time!. |
Record Nr. | UNINA-9910768447303321 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1997 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|
Tools and Algorithms for the Construction and Analysis of Systems [[electronic resource] ] : Second International Workshop, TACAS '96, Passau, Germany, March 27 - 29, 1996, Proceedings. / / edited by Tiziana Margaria, Bernhard Steffen |
Edizione | [1st ed. 1996.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1996 |
Descrizione fisica | 1 online resource (XIII, 443 p.) |
Disciplina | 004.2/1 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Computers
Operating systems (Computers) Computer logic Software engineering Computer communication systems Theory of Computation Operating Systems Logics and Meanings of Programs Software Engineering Computer Communication Networks |
ISBN | 3-540-49874-5 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Early fault detection tools -- Kleene algebra with tests and commutativity conditions -- Managing proofs -- An analyzer for message sequence charts -- Relation-algebraic analysis of Petri nets with RELVIEW -- Efficient search as a means of executing specifications -- An improvement of McMillan's unfolding algorithm -- Efficient local model-checking for fragments of the modal ?-calculus -- Test generation with inputs, outputs, and quiescence -- Breaking and fixing the Needham-Schroeder Public-Key Protocol using FDR -- Automatic compositional verification of some Security properties -- Permutable agents in process algebras -- Strategy construction in infinite games with Streett and Rabin chain winning conditions -- Timed Condition/Event systems: A framework for modular discrete models of chemical plants and verification of their real-time discrete control -- Formal verification of a partial-order reduction technique for model checking -- Fully automatic verification and error detection for parameterized iterative sequential circuits -- Priorities for modeling and verifying distributed systems -- Games and modal mu-calculus -- Generic system support for deductive program development -- Extending promela and spin for real time -- Reactive EFSMs — Reactive Promela/RSPIN -- Probabilistic duration automata for analyzing real-time systems -- The Concurrency Factory software development environment -- The Fc2Tools set (tool demonstration) -- PEP — more than a Petri Net tool -- Rapid prototyping for an assertional specification language -- cTc — A tool supporting the construction of cTLA-Specifications -- A tool for proving invariance properties of concurrent systems automatically -- Using the constraint language toupie for “Software Cost Reduction” specification analysis -- A constraint-oriented Service Creation Environment -- DFA&OPT-MetaFrame: A tool kit for program analysis and optimization -- A construction and analysis tool based on the stochastic process algebra TIPP -- Uppaal in 1995. |
Record Nr. | UNISA-996465574203316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1996 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|