Alessandro Cimatti
#145,896
Most Influential Person Now
Researcher
Alessandro Cimatti's AcademicInfluence.com Rankings
Alessandro Cimatticomputer-science Degrees
Computer Science
#7308
World Rank
#7697
Historical Rank
Automated Reasoning
#16
World Rank
#16
Historical Rank
Artificial Intelligence
#2953
World Rank
#2998
Historical Rank
Database
#4370
World Rank
#4544
Historical Rank
Download Badge
Computer Science
Alessandro Cimatti's Degrees
- PhD Computer Science University of Trento
- Masters Computer Science University of Bologna
- Bachelors Computer Science University of Bologna
Similar Degrees You Can Earn
Why Is Alessandro Cimatti Influential?
(Suggest an Edit or Addition)Alessandro Cimatti's Published Works
Number of citations in a given year to any of this author's works
Total number of citations to an author for the works they published in a given year. This highlights publication of the most important work(s) by the author
Published Works
- Symbolic Model Checking without BDDs (1999) (2516)
- NuSMV 2: An OpenSource Tool for Symbolic Model Checking (2002) (1615)
- NUSMV: a new symbolic model checker (2000) (803)
- Symbolic model checking using SAT procedures instead of BDDs (1999) (802)
- NUSMV: A New Symbolic Model Verifier (1999) (708)
- Nusmv version 2: an opensource tool for symbolic model checking (2002) (469)
- The MathSAT5 SMT Solver (2013) (450)
- The nuXmv Symbolic Model Checker (2014) (408)
- Weak, strong, and strong cyclic planning via symbolic model checking (2003) (386)
- Planning in Nondeterministic Domains under Partial Observability via Symbolic Model Checking (2001) (228)
- THE SINS SURVEY: MODELING THE DYNAMICS OF z ∼ 2 GALAXIES AND THE HIGH-z TULLY–FISHER RELATION (2009) (223)
- Safety, Dependability and Performance Analysis of Extended AADL Models (2011) (220)
- THE RADIAL AND AZIMUTHAL PROFILES OF Mg ii ABSORPTION AROUND 0.5 < z < 0.9 zCOSMOS GALAXIES OF DIFFERENT COLORS, MASSES, AND ENVIRONMENTS (2011) (193)
- Planning via Model Checking: A Decision Procedure for AR (1997) (179)
- A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions (2002) (173)
- Software model checking via large-block encoding (2009) (171)
- Conformant Planning via Symbolic Model Checking (2000) (169)
- Automatic OBDD-Based Generation of Universal Plans in Non-Deterministic Domains (1998) (167)
- Tracking the impact of environment on the galaxy stellar mass function up to z ~ 1 in the 10 k zCOSMOS sample (2009) (162)
- Formal Verification of Diagnosability via Symbolic Model Checking (2003) (149)
- Software Model Checking via IC3 (2012) (149)
- MBP: a Model Based Planner (2001) (139)
- Bounded Model Checking for Timed Systems (2002) (130)
- Verifying Industrial Hybrid Systems with MathSAT (2005) (120)
- Dynamical properties of AMAZE and LSD galaxies from gas kinematics and the Tully-Fisher relation at z~3 (2010) (116)
- Strong Planning in Non-Deterministic Domains Via Model Checking (1998) (116)
- RATSY - A New Requirements Analysis Tool with Synthesis (2010) (111)
- Automated Planning (2008) (108)
- The COMPASS Approach: Correctness, Modelling and Performability of Aerospace Systems (2009) (105)
- Efficient Interpolant Generation in Satisfiability Modulo Theories (2008) (102)
- Conformant planning via symbolic model checking and heuristic search (2004) (102)
- OCRA: A tool for checking the refinement of temporal contracts (2013) (101)
- IC3 Modulo Theories via Implicit Predicate Abstraction (2013) (101)
- MathSAT: Tight Integration of SAT and Mathematical Decision Procedures (2005) (94)
- Satisfiability Modulo the Theory of Costs: Foundations and Applications (2010) (94)
- Strong planning under partial observability (2006) (93)
- Efficient Satisfiability Modulo Theories via Delayed Theory Combination (2005) (90)
- The MathSAT 4SMT Solver (2008) (83)
- Verifying SystemC: A software model checking approach (2010) (82)
- An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic (2005) (81)
- Theory and Applications of Satisfiability Testing – SAT 2012 (2012) (79)
- A Property-Based Proof System for Contract-Based Design (2012) (78)
- Efficient theory combination via boolean search (2006) (77)
- Efficient generation of craig interpolants in satisfiability modulo theories (2009) (74)
- Heuristic Search + Symbolic Model Checking = Efficient Conformant Planning (2001) (71)
- Symbolic Fault Tree Analysis for Reactive Systems (2007) (70)
- Diagnostic Information for Realizability (2008) (70)
- Kratos - A Software Model Checker for SystemC (2011) (69)
- Conformant Planning via Model Checking (1999) (68)
- HyComp: An SMT-Based Model Checker for Hybrid Systems (2015) (68)
- The MathSAT 3 System (2005) (67)
- Contracts-refinement proof system for component-based embedded systems (2015) (65)
- Bounded Model Checking for Past LTL (2003) (65)
- Multi-Agent Reasoning with Belief Contexts: The Approach and a Case Study (1995) (64)
- A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories (2007) (64)
- Requirements Validation for Hybrid Systems (2009) (64)
- Spot the difference: Impact of different selection criteria on observed properties of passive galaxies in zCOSMOS-20k sample (2013) (63)
- The ALPINE-ALMA [CII] survey: Data processing, catalogs, and statistical source properties (2020) (63)
- Formal Verification of a Railway Interlocking System using Model Checking (1998) (62)
- A Lazy and Layered SMT ( B V ) Solver for Hard Industrial Verification Problems ⋆ (2007) (61)
- Modelling the number density of Hα emitters for future spectroscopic near-IR space missions (2016) (61)
- The Evolution of the Galaxy Luminosity Function in the Rest-Frame Blue Band up to z = 3.5 (2003) (61)
- Symbolic Computation of Schedulability Regions Using Parametric Timed Automata (2008) (60)
- The xSAP Safety Analysis Platform (2015) (58)
- The zCOSMOS 10k-sample: the role of galaxy stellar mass in the colour-density relation up to z ~ 1 (2010) (58)
- Formal Design and Safety Analysis of AIR6110 Wheel Brake System (2015) (57)
- Parameter synthesis with IC3 (2013) (56)
- Formal analysis of hardware requirements (2006) (56)
- Computing Predicate Abstractions by Integrating BDDs and SMT Solvers (2007) (55)
- The evolution of quiescent galaxies at high redshifts (z≥ 1.4) (2011) (55)
- Spacecraft early design validation using formal methods (2014) (54)
- The MathSAT 5 SMT Solver ⋆ (2012) (52)
- Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories (2014) (51)
- The VANDELS survey: the star-formation histories of massive quiescent galaxies at 1.0 < z < 1.3 (2019) (50)
- Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis (2006) (50)
- Solving Power Supply Restoration Problems with Planning via Symbolic Model Checking (2002) (48)
- Software Model Checking SystemC (2013) (47)
- The ALPINE–ALMA [C ii] Survey: Multiwavelength Ancillary Data and Basic Physical Measurements (2019) (47)
- Validation of requirements for hybrid systems: A formal approach (2012) (47)
- Verification of a safety-critical railway interlocking system with real-time constraints (1998) (46)
- SC2: Satisfiability Checking Meets Symbolic Computation - (Project Paper) (2016) (46)
- Improving the Encoding of LTL Model Checking into SAT (2002) (46)
- VIMOS Ultra-Deep Survey (VUDS): Witnessing the assembly of a massive cluster at z ~ 3.3 (2014) (46)
- The zCOSMOS redshift survey: the three-dimensional classification cube and bimodality in galaxy physical properties (2008) (44)
- The MathSAT 4 SMT Solver ( Tool Paper ) (2008) (43)
- Discovering extremely compact and metal-poor, star-forming dwarf galaxies out to z ∼ 0.9 in the VIMOS Ultra-Deep Survey (2014) (42)
- Model Checking Safety Critical Software with SPIN: An Application to a Railway Interlocking System (1998) (41)
- Bounded Verification of Past LTL (2004) (41)
- Encoding RTL Constructs for MathSAT: a Preliminary Report (2005) (41)
- A Framework for Planning with Extended Goals under Partial Observability (2003) (39)
- Formal Verification and Validation of ERTMS Industrial Railway Train Spacing System (2012) (39)
- A Lazy and Layered SMT($\mathcal{BV}$) Solver for Hard Industrial Verification Problems (2007) (39)
- SMT-based scenario verification for hybrid systems (2013) (39)
- A Modular Approach to MaxSAT Modulo Theories (2013) (39)
- Extending PDDL to nondeterminism, limited sensing and iterative conditional plans (2003) (39)
- THE DEPENDENCE OF STAR FORMATION ACTIVITY ON STELLAR MASS SURFACE DENSITY AND SERSIC INDEX IN zCOSMOS GALAXIES AT 0.5 < z < 0.9 COMPARED WITH SDSS GALAXIES AT 0.04 < z < 0.08 (2009) (38)
- Improving Heuristics for Planning as Search in Belief Space (2002) (38)
- An improved measurement of baryon acoustic oscillations from the correlation function of galaxy clusters at z ∼ 0.3 (2013) (38)
- Formalization and validation of a subset of the European Train Control System (2010) (37)
- Sound and Complete Algorithms for Checking the Dynamic Controllability of Temporal Networks with Uncertainty, Disjunction and Observation (2014) (37)
- Dynamic controllability via Timed Game Automata (2016) (36)
- Integrating BDD-Based and SAT-Based Symbolic Model Checking (2002) (36)
- Infinite-state invariant checking with IC3 and predicate abstraction (2016) (36)
- Boolean Abstraction for Temporal Logic Satisfiability (2007) (34)
- SAT-Based Bounded Model Checking for Timed Systems (2002) (34)
- A Model Checker for AADL (2010) (34)
- Applying SMT in symbolic execution of microcode (2010) (32)
- Model Checking at Scale: Automated Air Traffic Control Design Space Exploration (2016) (32)
- Symbolic Implementation of Alternating Automata (2006) (31)
- HyDI: A Language for Symbolic Hybrid Systems with Discrete Interaction (2011) (31)
- Verifying Heap-Manipulating Programs in an SMT Framework (2007) (30)
- Formal Verification of Infinite-State BIP Models (2015) (30)
- Verifying LTL Properties of Hybrid Systems with K-Liveness (2014) (30)
- Codesign of dependable systems: A component-based modeling language (2009) (29)
- Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions (2018) (29)
- An Integrated Process for FDIR Design in Aerospace (2014) (29)
- Timelines with Temporal Uncertainty (2013) (29)
- A Provably Correct Embedded Verifier for the Certification of Safety Critical Software (1997) (29)
- Formalizing requirements with object models and temporal constraints (2011) (29)
- Formal Verification and Validation of AADL Models (2010) (29)
- Dust attenuation in z $\sim$ 1 galaxies from Herschel and 3D-HST H$\alpha$ measurements (2015) (28)
- From PSL to NBA: a Modular Symbolic Encoding (2006) (28)
- Interpolant Generation for UTVPI (2009) (28)
- To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in SMT(EUF ÈT) (2006) (28)
- Efficient Anytime Techniques for Model-Based Safety Analysis (2015) (27)
- Symbolic execution with existential second-order constraints (2018) (27)
- Time-aware relational abstractions for hybrid systems (2013) (27)
- A journey from the outskirts to the cores of groups : I. Color- and mass-segregation in 20K-zCOSMOS groups (2012) (27)
- Boosting Lazy Abstraction for SystemC with Partial Order Reduction (2011) (27)
- Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF (2017) (27)
- Solving strong controllability of temporal problems with uncertainty using SMT (2014) (27)
- The VANDELS survey: dust attenuation in star-forming galaxies at z=3-4 (2017) (26)
- Safety assessment of AltaRica models via symbolic model checking (2015) (26)
- The ALPINE-ALMA [CII] survey: Molecular gas budget in the Early Universe as traced by [CII] (2020) (25)
- A quantifier-free SMT encoding of non-linear hybrid automata (2012) (25)
- Interleaving Execution and Planning for Nondeterministic, Partially Observable Domains (2004) (24)
- Symbolic Synthesis of Observability Requirements for Diagnosability (2012) (24)
- SMT-Based Verification of Hybrid Systems (2012) (24)
- Beyond Boolean SAT: Satisfiability modulo theories (2008) (23)
- Verilog2SMV: A tool for word-level verification (2016) (23)
- Combining MILS with Contract-Based Design for Safety and Security Requirements (2014) (23)
- Using Timed Game Automata to Synthesize Execution Strategies for Simple Temporal Networks with Uncertainty (2014) (23)
- Formal Safety Assessment via Contract-Based Design (2014) (22)
- Proving and explaining the unfeasibility of Message Sequence Charts for hybrid systems (2011) (21)
- From Informal Requirements to Property-Driven Formal Validation (2009) (21)
- RTL VERIFICATION: FROM SAT TO SMT(BV) (2008) (21)
- Model Checking of Hybrid Systems Using Shallow Synchronization (2010) (21)
- Introspective Metatheoretic Reasoning (1994) (20)
- Symbolic Compilation of PSL (2008) (20)
- Passive galaxies as tracers of cluster environments at z~2 (2015) (20)
- Symbolic Model Checking and Safety Assessment of Altarica models (2012) (20)
- Solving Temporal Problems Using SMT: Strong Controllability (2012) (20)
- Industrial Applications of Model Checking (2000) (19)
- Symbolic Model Checking for Multi-Agent Systems (2007) (19)
- HRELTL: A temporal logic for hybrid systems (2015) (19)
- Beyond the Single Planning Paradigm: Introspective Planning (1992) (19)
- Obscured AGN at 1.5 < z < 3.0 from the zCOSMOS-deep Survey (2019) (19)
- Many Hands Make Light Work: Localized Satisfiability for Multi-Context Systems (2004) (18)
- Strong Temporal Planning with Uncontrollable Durations: A State-Space Approach (2015) (18)
- Strong temporal planning with uncontrollable durations (2018) (18)
- Comparing different functional allocations in automated air traffic control design (2015) (18)
- Formal Design of Fault Detection and Identification Components Using Temporal Epistemic Logic (2014) (18)
- Integrating Boolean and Mathematical Solving: Foundations, Basic Algorithms, and Requirements (2002) (18)
- Dynamic Controllability of Disjunctive Temporal Networks: Validation and Synthesis of Executable Strategies (2016) (18)
- Efficient Scenario Verification for Hybrid Automata (2011) (17)
- Formal Specification and Development of a Safety-Critical Train Management System (1999) (17)
- SMT-Based Validation of Timed Failure Propagation Graphs (2015) (17)
- Satisfiability Modulo Transcendental Functions via Incremental Linearization (2017) (17)
- Simulating the physics and mass assembly of distant galaxies out to z∼ 6 with the E-ELT (2009) (17)
- A Comprehensive Approach to On-board Autonomy Verification and Validation (2011) (17)
- Structure-aware computation of predicate abstraction (2009) (17)
- Supporting Requirements Validation: The EuRailCheck Tool (2009) (16)
- Parametric analysis of distributed firm real-time systems: A case study (2010) (16)
- Multiagent Reasoning with Belief Contexts II: Elaboration Tolerance (1995) (15)
- A Symbolic Model Checking Framework for Safety Analysis, Diagnosis, and Synthesis (2007) (15)
- Formal Design of Asynchronous Fault Detection and Identification Components using Temporal Epistemic Logic (2015) (15)
- Formalization and Validation of Safety-Critical Requirements (2010) (15)
- The zCOSMOS redshift survey : Influence of luminosity, mass and environment on the galaxy merger rate (2011) (15)
- Euclid: Impact of non-linear and baryonic feedback prescriptions on cosmological parameter estimation from weak lensing cosmic shear (2020) (15)
- Infinite-State Liveness-to-Safety via Implicit Abstraction and Well-Founded Relations (2016) (14)
- Solving Temporal Problems Using SMT: Weak Controllability (2012) (14)
- Formal Methods for Hardware Verification, 6th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2006, Bertinoro, Italy, May 22-27, 2006, Advanced Lectures (2006) (14)
- An Analytic Evaluation of SystemC Encodings in Promela (2011) (14)
- Extending nuXmv with Timed Transition Systems and Timed Temporal Properties (2019) (14)
- A GROUP-GALAXY CROSS-CORRELATION FUNCTION ANALYSIS IN zCOSMOS (2012) (13)
- Semi-ProtoPNet Deep Neural Network for the Classification of Defective Power Grid Distribution Structures (2022) (13)
- Searching Powerset Automata by Combining Explicit-State and Symbolic Model Checking (2001) (13)
- System-Software Co-Engineering: Dependability and Safety Perspective (2011) (13)
- Automated Synthesis of Timed Failure Propagation Graphs (2016) (13)
- Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization (2018) (13)
- Assumption-Based Runtime Verification with Partial Observability and Resets (2019) (13)
- The ALPINE-ALMA [C ii] survey: a triple merger at z ∼ 4.56 (2019) (13)
- Model-Based Codesign of Critical Embedded Systems (2009) (13)
- Verification and performance evaluation of aadl models (2009) (12)
- The NIRVANDELS Survey: a robust detection of α-enhancement in star-forming galaxies at z ≃ 3.4 (2021) (12)
- An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty (2015) (12)
- Automated Verification and Tightening of Failure Propagation Models (2016) (12)
- Tighter integration of BDDs and SMT for Predicate Abstraction (2010) (11)
- Software Model Checking with Explicit Scheduler and Symbolic Threads (2012) (11)
- Validating Domains and Plans for Temporal Planning via Encoding into Infinite-State Linear Temporal Logic (2017) (11)
- Formal specification of beliefs in multi-agent systems (1996) (11)
- The ALPINE-ALMA [C II] Survey: [C II] 158 μm Emission Line Luminosity Functions at z ∼ 4–6 (2020) (11)
- Galaxy evolution in overdense environments at high redshift: passive early-type galaxies in a cluster at redshift 2 (2021) (11)
- Validation of Multiagent Systems by Symbolic Model Checking (2002) (10)
- Automated Analysis of Reliability Architectures (2013) (10)
- Requirements Refinement and Component Reuse: The FoReVer Contract-Based Approach (2014) (10)
- Object Models with Temporal Constraints (2008) (10)
- The ALPINE−ALMA [C ii] Survey: on the nature of an extremely obscured serendipitous galaxy (2020) (10)
- Analysis of Relay Interlocking Systems via SMT-based Model Checking of Switched Multi-Domain Kirchhoff Networks (2018) (10)
- The bimodality of the 10k zCOSMOS-bright galaxies up to z ~ 1: a new statistical and portable classification based on optical galaxy properties (2010) (10)
- On the robustness of the Hβ Lick index as a cosmic clock in passive early-type galaxies (2017) (9)
- Dealing With Expected and Unexpected Obstacles (1997) (9)
- Formal Methods for Aerospace Systems (2017) (9)
- Compass 3.0 (2019) (9)
- Formal Specification and Verification of Dynamic Parametrized Architectures (2018) (8)
- Syntactic Optimizations for PSL Verification (2007) (8)
- Implementing Planning As Tactical Reasoning (1992) (8)
- Towards Strong Cyclic Planning under Partial Observability (2006) (8)
- The MathSAT Solver — a progress report (2004) (8)
- Formal Specification and Validation of a Vital Communication Protocol (1999) (8)
- Unveiling the inner morphology and gas kinematics of NGC 5135 with ALMA (2017) (8)
- Navigation by combining reactivity and planning (1992) (8)
- ON-BOARD AUTONOMY VIA SYMBOLIC MODEL-BASED REASONING ∗ (2008) (8)
- Building Efficient Decision Procedures on Top of SAT Solvers (2006) (8)
- Towards Pareto-optimal parameter synthesis for monotonie cost functions (2014) (8)
- Efficient Analysis of Reliability Architectures via Predicate Abstraction (2013) (7)
- Building and Executing Proof Strategies in a Formal Metatheory (1993) (7)
- itc . it PLAN VALIDATION FOR EXTENDED GOALS UNDER PARTIAL OBSERVABILITY ( PRELIMINARY REPORT (2002) (7)
- SMT-based satisfiability of first-order LTL with event freezing functions and metric operators (2020) (7)
- Visual representation of natural language scene descriptions (1996) (7)
- Temporal Planning with Intermediate Conditions and Effects (2019) (6)
- ARCH-COMP19 Category Report: Hybrid Systems with Piecewise Constant Dynamics (2019) (6)
- Measuring galaxy environment with the synergy of future photometric and spectroscopic surveys (2016) (6)
- OthelloPlay: a plug-in based tool for requirement formalization and validation (2011) (6)
- Abstraction in Planning via Model Checking (1998) (6)
- Satisfiability checking and symbolic computation (2016) (6)
- Robustness Envelopes for Temporal Plans (2019) (6)
- From Electrical Switched Networks to Hybrid Automata (2016) (6)
- Stong Cyclic Planning Under Partial Observability (2006) (6)
- Reactive Synthesis from Extended Bounded Response LTL Specifications (2020) (5)
- Quantifier-free encoding of invariants for hybrid systems (2014) (5)
- Timed Failure Propagation Analysis for Spacecraft Engineering: The ESA Solar Orbiter Case Study (2017) (5)
- Universal Invariant Checking of Parametric Systems with Quantifier-free SMT Reasoning (2021) (5)
- Mechanizing Multi-Agent Reasoning with Belief Contexts (1996) (5)
- A Formal Framework for the Specification, Verification and Synthesis of Diagnosers (2013) (5)
- Automated Planning and Model Checking (Dagstuhl Seminar 14482) (2015) (5)
- A Temporal Logics Approach to Contract-Based Design (2016) (5)
- Verification of parametric system designs (2012) (5)
- The Mobile Robot of MAIA: Actions and Interactions in a Real Life Scenario (1995) (5)
- A Lazy Approach to Temporal Epistemic Logic Model Checking (2016) (5)
- Euclid: Effects of sample covariance on the number counts of galaxy clusters (2021) (4)
- FAME Process: A Dedicated Development and V&V Process for FDIR (2014) (4)
- Extended bounded response LTL: a new safety fragment for efficient reactive synthesis (2021) (4)
- NuSMV Version 2: BDD-based + SAT-based Symbolic Model Checking (2001) (4)
- Computation of the Transient in Max-Plus Linear Systems via SMT-Solving (2020) (4)
- Formal Analysis ofHardware Requirements (2006) (4)
- Programming Planners with Flexible Architectures (1993) (4)
- 5 Conclusions and Future Work (1997) (4)
- A Model-Based Approach to the Design, Verification and Deployment of Railway Interlocking System (2020) (4)
- A Many‐Sorted Natural Deduction (1998) (4)
- Flexible planning by integrating multilevel reasoning (1995) (3)
- Parameter Synthesis with IC 3 (2015) (3)
- SMT-based analysis of switching multi-domain linear Kirchhoff networks (2017) (3)
- A Structured Approach to the Formal Certification of Safety of Computer Aided Development Tools (1998) (3)
- Formal reliability analysis of redundancy architectures (2019) (3)
- Implicit Semi-Algebraic Abstraction for Polynomial Dynamical Systems (2021) (3)
- Tightening a Contract Refinement (2016) (3)
- NuRV: A nuXmv Extension for Runtime Verification (2019) (3)
- The ALPINE-ALMA [C ii] Survey: kinematic diversity and rotation in massive star-forming galaxies at z ~ 4.4–5.9 (2021) (3)
- Proving the Existence of Fair Paths in Infinite-State Systems (2021) (3)
- Computational reflection via mechanized logical deduction (1996) (3)
- The FoReVer Methodology: A MBSE Framework for Formal Verification (2013) (3)
- Tightening the contract refinements of a system architecture (2018) (3)
- Incremental linearization: A practical approach to satisfiability modulo nonlinear arithmetic and transcendental functions (2018) (3)
- Interleaving Execution and Planning via Symbolic Model Checking (2007) (3)
- MRG: Building planers for real-world complex applications (1994) (3)
- Euclid: the selection of quiescent and star-forming galaxies using observed colours (2020) (2)
- Improved Decision Heuristics for High Performance SAT Based Static Property Checking (2004) (2)
- Expressiveness of Extended Bounded Response LTL (2021) (2)
- Conditional Planning under Partial Observability as Heuristic-Symbolic Search in Belief Space (2014) (2)
- Assumption-Based Runtime Verification of Infinite-State Systems (2021) (2)
- SMT-based scenario verification for hybrid systems (2012) (2)
- $$\mathsf {SC}^\mathsf{2} $$: Satisfiability Checking Meets Symbolic Computation (2016) (2)
- Proceedings of the 15th international conference on Theory and Applications of Satisfiability Testing (2012) (2)
- zCOSMOS 10 k-bright spectroscopic sample Exploring mass and environment dependence in early-type galaxies (2010) (2)
- Model-Based Run-Time Synthesis of Architectural Configurations for Adaptive MILS Systems (2019) (2)
- Euclid: Forecasts for k-cut 3×2 Point Statistics (2020) (2)
- A comprehensive framework for the analysis of automotive systems (2022) (1)
- A CEGAR-based Approach for Proving Invariant Properties of Transition Systems on Non-Linear Real Arithmetic ( Extended Abstract ) (2016) (1)
- Model-based Safety Assessment of a Triple Modular Generator with xSAP (2021) (1)
- RATOS – A Software Model Checker for SystemC (1)
- Dust attenuation in z ∼ 1 galaxies from Herschel and 3D-HST H α measurements (2015) (1)
- Handling Polynomial and Transcendental Functions in SMT via Unconstrained Optimisation and Topological Degree Test (2022) (1)
- Conformant Planning via Model Checking Limited Distribution Notice (1999) (1)
- SC2: Satisfiability Checking Meets Symbolic Computation (Project Paper) (2016) (1)
- SMT-Based Software Model Checking (2010) (1)
- Reverse engineering with P-stable Abstractions (2021) (1)
- From Electrical Switched Networks to Hybrid Automata ( Extended Version ) (2016) (1)
- The ALPINE-ALMA [CII] Survey: nature, luminosity function and star formation history of continuum non-target galaxies up to z~6 (2020) (1)
- A Data-driven Approach for RUL Prediction of an Experimental Filtration System (2020) (1)
- A Comparison between Vector Quantization and Hidden Markov Mod- Els in Text Independent Speech Recognition Systems. Irst (1)
- Model-Based Design of an Energy-System Embedded Controller Using Taste (2016) (1)
- Efficiently Integrating Boolean Reasoning and Mathematical Solving (2003) (1)
- University of Trento Software Model Checking via Large-block Encoding Software Model Checking via Large-block Encoding (2009) (1)
- Application of SMT solvers to hybrid system verification (2012) (1)
- Innovative Rover Operations Concepts - Autonomous Planner (IRONCAP) - Concluding the adventure (2014) (1)
- Scheduling optimisations for SPIN to minimise buffer requirements in synchronous data flow (2009) (1)
- Verification and Performance Evaluation of AADL Models (Tool Demonstration) (2009) (1)
- Satisfiability Checking meets Symbolic Computation (Project Paper) (2016) (1)
- Diagnosability of fair transition systems (2022) (1)
- Innovative Rover Operations Concepts – Autonomous Planning Keeping a dog on the lead (2011) (1)
- The E-ELT Design Reference Mission: The physics and mass assembly of galaxies out to z∼6 Results of Simulations (2008) (1)
- SC 2 : Satisfiability Checking meets (2016) (1)
- A first-order logic characterisation of safety and co-safety languages (2022) (1)
- Integrating formal methods into the development cycle of a safety-critical embedded software system (2000) (1)
- Synthesis of P-Stable Abstractions (2020) (1)
- The ALPINE-ALMA [CII] survey. No or weak evolution in the [CII]-SFR relation over the last 13 Gyr (2020) (1)
- NORMA: a tool for the analysis of Relay-based Railway Interlocking Systems (2022) (1)
- Efficient Solving of the Satisfiability Modulo Bit-Vectors Problem and Some Extensions to SMT (2010) (0)
- GR(1) is equivalent to R(1) (2023) (0)
- VizieR Online Data Catalog: VUDS extreme emission line 0.2\lt~z\lt~0.9 galaxies (Amorin+, 2014) (2014) (0)
- Formal Methods in Computer-Aided Design, FMCAD 2008, Portland, Oregon, USA, 17-20 November 2008 (2008) (0)
- 5 Mixing Reasoning at Diierent Levels 4 Metatheoretic Reasoning (1990) (0)
- Ultra Deep Survey first data release : Spectra and spectroscopic redshifts of 698 objects up to z spec ∼ 6 in CANDELS ? , ? ? (2017) (0)
- Safe Decomposition of Startup Requirements: Verification and Synthesis (2020) (0)
- Istituto per La Ricerca Scientifica E Tecnologica Certification of Translators via Off- Line and On-line Proof Logging and Checking Certiication of Translators via Oo-line and On-line Proof Logging and Checking (2007) (0)
- SC-square: when Satisfiability Checking and Symbolic Computation join forces (2017) (0)
- Towards Efficient Anytime Computation and Execution of Decoupled Robustness Envelopes for Temporal Plans (2019) (0)
- <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" altimg="si1.svg"><mml:mrow><mml:mi mathvariant="sans-serif">GR</mml:mi></mml:mrow><mml:mo stretchy="false">(</mml:mo><mml:mn>1</mml:mn><mml:mo stretchy="false">)</mml:mo></mml:math> is equivalent to <mml:math xmlns:mml="http://www.w3.org/1998/ (2022) (0)
- VizieR Online Data Catalog: VUDS Dicovery of a high-redshift protocluster (Lemaux+, 2014) (2014) (0)
- SystemC design Thread T 3 Thread T 2 Thread T 1 ESST Abstract Reachability Tree ( ART ) (2011) (0)
- Deciding Unsolvability in Temporal Planning under Action Non-Self-Overlapping (2022) (0)
- Parameter Synthesis with IC3 (Informal Presentation) (2015) (0)
- Computer Aided Modelling and Simulation of Complex Mechanical Systems (1989) (0)
- Verification of SMT Systems with Quantifiers (2022) (0)
- Exemplary Achievements SC 2 challenges : when Satisfiability Checking and Symbolic Computation join forces (2017) (0)
- S C ] 2 3 Ju l 2 01 6 Satisfiability Checking and Symbolic Computation (2016) (0)
- The zCOSMOS-Bright survey: the clustering of galaxy morphological types since z~1 (2009) (0)
- War87] K. Warren. Implementation of a Deenition Expansion Mechanism in a Connec- Tion Method Theorem Prover. Master's Thesis (0)
- Formal reliability analysis of redundancy architectures (2019) (0)
- Efficient Analysis of Cyclic Redundancy Architectures via Boolean Fault Propagation (2022) (0)
- Project DEPLOY Grant Agreement 214158 “ Industrial deployment of advanced system engineering methods for high productivity and dependability ” DEPLOY Deliverable D 32 D 9 . 3 Model Construction Tools and Analysis Tools III (2011) (0)
- VIMOS Ultra-Deep Survey (VUDS): Witnessing the Assembly of a Massive Cluster at <em>z</em> ~ 3.3 (2019) (0)
- Model checking: teoria ed applicazioni (2018) (0)
- An Analysis of the Prevalence of Cookies on the World Wide Web (2000) (0)
- SMT-Based Software Model Checking - Explicit Scheduler, Symbolic Threads (2013) (0)
- Searching for Ribbon-Shaped Paths in Fair Transition Systems (2022) (0)
- 28th International Workshop on Principles of Diagnosis (DX'17), Brescia, Italy, September 26-29, 2017 (2018) (0)
- Solving strong controllability of temporal problems with uncertainty using SMT (2014) (0)
- Forward Conformant Planning via Symbolic Model Checking (2007) (0)
- Efficient SMT-Based Analysis of Failure Propagation (2021) (0)
- Lemmas for Satisfiability Modulo Transcendental Functions via Incremental Linearization ( extended abstract ) (2019) (0)
- Formal Design and Validation of an Automatic Train Operation Control System (2022) (0)
- References 5 Conclusions and Future Work (1997) (0)
- Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design (2008) (0)
- C Proof of Theorem 4 . 1 a Proof of Theorem 3 . 1 (1994) (0)
- Contract-based Design: a Temporal Logics Approach (2013) (0)
- First Steps Towards Correct System Synthesis of System Code (1995) (0)
- The bimodality of the 10k zCOSMOS-bright galaxies up to z similar to 1 (2011) (0)
- Automatic Discovery of Fair Paths in Infinite-State Transition Systems (2021) (0)
- Bounded Model Checking for Timed Systems Limited Distribution Notice (2002) (0)
- Software Engineering and Formal Methods (2017) (0)
- Predicting RUL of Bearings in the Pumps of a Critical Industrial Air Treatment System (2020) (0)
- EVA: a Tool for the Compositional Verification of AUTOSAR Models (2023) (0)
- S C ] 2 7 Ju l 2 01 6 SC 2 : Satisfiability Checking meets Symbolic Computation ( Project Paper ) (2016) (0)
- The VMT-LIB Language and Tools (2021) (0)
- Proceedings of the 6th international conference on Formal Methods for the Design of Computer, Communication, and Software Systems (2006) (0)
- Temporal logic satisfiability for the design of complex systems: Invited Presentation at the Fourth International Symposium on Games, Automata, Logics and Formal Verification (2013) (0)
- Dynamic controllability via Timed Game Automata (2016) (0)
- The MathSAT Solver — a progress report ( Extended Abstract ) (2004) (0)
- Requirements Analysis Tool Authors (2006) (0)
- SMT-Based Model Checking of Max-Plus Linear Systems (2021) (0)
- Infinite-state invariant checking with IC3 and predicate abstraction (2016) (0)
- From Informal Safety-Critical Requirements to Property-Driven Formal Validation (2008) (0)
- 2008 formal methods in computer aided design, Portland, Oregon, USA, 17-20 November 2008 (2008) (0)
- University of Groningen Obscured AGN at 1.5 <z <3.0 from the zCOSMOS-deep Survey I. Properties of the emitting gas in the narrow-line region Mignoli, (2019) (0)
- itc . it IMPROVING HEURISTICS FOR PLANNING AND SEARCH IN BELIEF (2001) (0)
- Towards a Theory of Embedded Planning (1993) (0)
- Optimization Modulo Non-linear Arithmetic via Incremental Linearization (2021) (0)
- Abstraction Modulo Stability for Reverse Engineering (2022) (0)
- Fairness, Assumptions, and Guarantees for Extended Bounded Response LTL+P Synthesis (2021) (0)
- Quantifier-free encoding of invariants for hybrid systems (2013) (0)
- VizieR Online Data Catalog: Obscured AGN at 1.5 (2019) (0)
- Assumption-based Runtime Verification (2022) (0)
- Symbolic Encoding of Reliability for the Design of Redundant Architectures (2022) (0)
- The VIMOS Ultra Deep Survey: 10 000 Galaxies to Study the Early Phases of Galaxy Assembly at 2 < z < 6+ (2014) (0)
- 4 Extensions and Future Work 3.3 Symbolic Layer (2007) (0)
- Intelligent Computer Mathematics (2016) (0)
- Tightening the contract refinements of a system architecture (2018) (0)
- Towards adaptive MILS System: Model- Based Design, Verification and Run-Time Adaptation: Slides (2018) (0)
- LTL falsification in infinite-state systems (2022) (0)
- A Context-Based Mechanization of Multi-Agent Reasoning (2000) (0)
- itc . it MBP : A MODEL BASED (2007) (0)
- The star formation rate cookbook at 1 (2018) (0)
- Analysis of Cyclic Fault Propagation via ASP (2022) (0)
- SAT 2005; Satisfiability Research in the Year 2005 (2006) (0)
- From Sequential Extended Regular Expressions to NFA with Symbolic Labels (2010) (0)
- X-ray emission from He II 1640 emitting galaxies in VANDELS (2020) (0)
- VizieR Online Data Catalog: The zCOSMOS 10k-bright spectroscopic sample (Lilly+, 2009) (2010) (0)
- Aknowledgments 5.3 Deducing in Ot via Reasoning in Mt (1994) (0)
- A Formal IDE for Railways: Research Challenges (2022) (0)
- COMPASTA: Extending TASTE with Formal Design and Verification Functionality (2022) (0)
- Automatic Design Space Exploration of Redundant Architectures (2021) (0)
- Computing Small Unsatisable Cores in Satisability Modulo Theories (2011) (0)
This paper list is powered by the following services:
What Schools Are Affiliated With Alessandro Cimatti?
Alessandro Cimatti is affiliated with the following schools:
