费尔南多·佩索阿在里斯本的天空上写着：“我们活过的刹那，前后皆是暗夜。”暗夜是永久的，可以大到无限，可以小到没有，星辰是久远之前的星辰。出门之后，我在寓所门外，伫立，觉得自己的生活一塌糊涂，当下即是糟糕，任何酒任何烟任何景色任何香吻都无法弥补莫名其妙的空缺，暑天长长的日头令人眩晕，没有角落会暗孕出一片风，没有人会在深夜过后的清晨说想你，大抵是繁忙，充斥在时间和往来肉体的每条缝。柳条，也不懂得勾引我了，是到中年了吧。又觉自己的生活无比丰美，当下即是未来，拔出傲剑，就有一道光，迈开腿，天就禁不住垂泪，任由冰雨在脸上无情得拍。外甥女无意间对我说，黑夜是最长的影子。才知晓孩子永远是最上等的诗人。
优秀的电影和文学作品，看完之后总是让人思绪万千，但同时，又从来找不到任何合适的方式表达积蓄的情感。我已经越来越不想去影院看电影了，男人快乐的方式其实也没有那么多，如今又少了一样。黑暗的环境，温暖的座椅，边上陌生女孩十分淡雅的香气，脑子里没有多余的细胞去思索她的性情编织她背后的荒原，总之，不到五分钟就在座椅上就颠了，睡死了，头就像一个延迟的不倒翁或者摆钟，一会倒在左边，一会倒在右边，加上轰鸣的音效，反而是一种类似白噪音的效果，睡半小时，仿佛睡了一整晚，模糊的意识中，冒出一些字：
Diffblue 团队在 CAV'18 发表了工具文章，JBMC。这个工具是 CBMC 的扩展，目的是验证 JAVA Bytecode。JBMC 的步骤和 CBMC 类似，也是前端处理程序，转换程序到公式，然后公式传递给求解器。
JBMC 的验证步骤：
