Travelled to:1 × Denmark
1 × Switzerland
2 × USA
3 × Italy
Collaborated with:Z.Manna M.Colón S.Sankaranarayanan T.E.Uribe N.Bjørner A.Browne E.Y.Chang A.Kapur L.d.Alfaro H.Devarajan J.Lee
Talks about:linear (4) generat (2) tempor (2) system (2) invari (2) deduct (2) verif (2) step (2) use (2) non (2)
Person: Henny Sipma
DBLP: Sipma:Henny
Contributed to:
2004
20032002
2001
200019991996
1995Wrote 9 papers:
- POPL-2004-SankaranarayananSM #generative #invariant #using
- Non-linear loop invariant generation using Gröbner bases (SS, HS, ZM), pp. 318–329.
- CAV-2003-ColonSS #constraints #generative #invariant #linear #theorem proving #using
- Linear Invariant Generation Using Non-linear Constraint Solving (MC, SS, HS), pp. 420–432.
- CAV-2002-ColonS #proving #termination
- Practical Methods for Proving Program Termination (MC, HS), pp. 442–454.
- TACAS-2001-ColonS #linear #ranking #synthesis
- Synthesis of Linear Ranking Functions (MC, HS), pp. 67–81.
- ICALP-2000-MannaS #safety
- Alternating the Temporal Picture for Safety (ZM, HS), pp. 429–450.
- CAV-1999-MannaS #diagrams #induction #verification
- Verification of Parameterized Systems by Dynamic Induction on Diagrams (ZM, HS), pp. 25–41.
- CAV-1996-BjornerBCCKMSU #named #realtime #verification
- STeP: Deductive-Algorithmic Verification of Reactive and Real-Time Systems (NB, AB, EYC, MC, AK, ZM, HS, TEU), pp. 415–418.
- CAV-1996-SipmaUM #deduction #model checking
- Deductive Model Checking (HS, TEU, ZM), pp. 208–219.
- TAPSOFT-1995-MannaBBCCADKLSU #named #proving
- STeP: The Stanford Temporal Prover (ZM, NB, AB, EYC, MC, LdA, HD, AK, JL, HS, TEU), pp. 793–794.