Travelled to:1 × Estonia
1 × France
1 × Germany
1 × New Zealand
1 × United Kingdom
1 × Uruguay
2 × Italy
Collaborated with:B.Fischer J.Morse D.Nicole R.S.Barreto F.R.Monteiro H.Rocha P.Kesseli D.Kroening M.Y.R.Gadelha D.A.Nicole J.Marques-Silva A.D.Neto F.Cruz P.R.M.Maciel M.A.P.Garcia E.B.d.L.Filho A.Abate I.Bessa D.Cattaruzza C.David E.Polgreen M.Ramalho P.Schrammel M.Trtík B.F.0002 L.C.Chaves
Talks about:model (9) check (7) bound (7) softwar (4) esbmc (4) contribut (3) synthesi (3) competit (3) program (3) tool (3)
Person: Lucas C. Cordeiro
DBLP: Cordeiro:Lucas_C=
Contributed to:
2015
20142013
201220122011
2009
200820172018
2018
20172018Wrote 14 papers:
- SEFM-2015-RochaBC #bound #c #generative #memory management #model checking #source code #testing #using
- Memory Management Test-Case Generation of C Programs Using Bounded Model Checking (HR, RSB, LCC), pp. 251–267.
- TACAS-2014-MorseRCN0 #contest
- ESBMC 1.22 — (Competition Contribution) (JM, MR, LCC, DN, BF), pp. 405–407.
- TACAS-2013-MorseCNF #bound #contest
- Handling Unbounded Loops with ESBMC 1.20 — (Competition Contribution) (JM, LCC, DN, BF), pp. 619–622.
- IFM-2012-RochaBCN #bound #comprehension #debugging #model checking #programming #using
- Understanding Programming Bugs in ANSI-C Software Using Bounded Model Checking Counter-Examples (HR, RSB, LCC, ADN), pp. 128–142.
- TACAS-2012-CordeiroMNF #bound #contest #model checking
- Context-Bounded Model Checking with ESBMC 1.17 — (Competition Contribution) (LCC, JM, DN, BF), pp. 534–537.
- SEFM-2011-MorseCNF #bound #ltl #model checking
- Context-Bounded Model Checking of LTL Properties for ANSI-C Software (JM, LCC, DN, BF), pp. 302–317.
- ASE-2009-CordeiroFM #bound #embedded #model checking #smt
- SMT-Based Bounded Model Checking for Embedded ANSI-C Software (LCC, BF, JMS), pp. 137–148.
- DATE-2008-CruzBCM #embedded #modelling #named #realtime #synthesis
- ezRealtime: A Domain-Specific Modeling Tool for Embedded Hard Real-Time Software Synthesis (FC, RSB, LCC, PRMM), pp. 1510–1515.
- ASE-2017-AbateBCCCDKKP #automation #named #physics #synthesis
- DSSynth: an automated digital controller synthesis tool for physical plants (AA, IB, DC, LCC, LCC, CD, PK, DK, EP), pp. 919–924.
- ASE-2018-GadelhaMMC0N #c #model checking
- ESBMC 5.0: an industrial-strength C model checker (MYRG, FRM, JM, LCC, BF0, DAN), pp. 888–891.
- ASE-2018-MonteiroGCF #bound #c++ #framework #model checking #platform #source code
- Bounded model checking of C++ programs based on the Qt cross-platform framework (journal-first abstract) (FRM, MAPG, LCC, EBdLF), p. 954.
- ESEC-FSE-2018-GadelhaMCN #debugging #detection #performance #towards
- Towards counterexample-guided k-induction for fast bug detection (MYRG, FRM, LCC, DAN), pp. 765–769.
- CAV-2017-AbateBCCDKKP #automation #physics #synthesis
- Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants (AA, IB, DC, LCC, CD, PK, DK, EP), pp. 462–482.
- CAV-2018-CordeiroKKST #bound #bytecode #java #model checking #named #verification
- JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode (LCC, PK, DK, PS, MT), pp. 183–190.